1  /-
  2  Copyright (c) 2018 Chris Hughes. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Chris Hughes
  5  -/
  6  
  7  import field_theory.finite data.zmod.basic data.nat.parity
src         └─────────────────┘ └─────────────┘ └─────────────┘
  8  
  9  /-!
 10  # Quadratic reciprocity.
 11  
 12  This file contains results about quadratic residues modulo a prime number.
 13  
 14  The main results are the law of quadratic reciprocity, `quadratic_reciprocity`, as well as the
 15  interpretations in terms of existence of square roots depending on the congruence mod 4,
 16  `exists_pow_two_eq_prime_iff_of_mod_four_eq_one`, and
 17  `exists_pow_two_eq_prime_iff_of_mod_four_eq_three`.
 18  
 19  Also proven are conditions for `-1` and `2` to be a square modulo a prime,
 20  `exists_pow_two_eq_neg_one_iff_mod_four_ne_three` and
 21  `exists_pow_two_eq_two_iff`
 22  
 23  ## Implementation notes
 24  
 25  The proof of quadratic reciprocity implemented uses Gauss' lemma and Eisenstein's lemma
 26  -/
 27  
 28  
 29  open function finset nat finite_field zmodp
 30  
 31  namespace zmodp
 32  
 33  variables {p q : ℕ} (hp : nat.prime p) (hq : nat.prime q)
id                            └───────┘          └───────┘
src                           └───────┘          └───────┘
typ                           └───────┘          └───────┘
doc                            └───────┘          └───────┘
 34  
 35  @[simp] lemma card_units_zmodp : fintype.card (units (zmodp p hp)) = p - 1 :=
id                                    └──────────┘  └───┘  └───┘  └┘     
src                                   └──────────┘  └───┘  └───┘           
typ                                   └──────────┘  └───┘  └───┘  └┘     
doc    └──┘                           └──────────┘
 36  by rw [card_units, card_zmodp]
id          └────────┘  └────────┘
src     └──┘└────────┘└┘└────────┘└─
typ     └──┘└────────┘└┘└────────┘└─
doc     └──┘          └┘          └─
txt     └──┘          └┘          └─
par     └──┘          └┘          └─
pid       └┘          └┘          
st     └─────────────┘└──────────┘
 37  
src  
typ  
doc  
txt  
par  
pid  
st   
 38  theorem fermat_little {p : ℕ} (hp : nat.prime p) {a : zmodp p hp} (ha : a ≠ 0) : a ^ (p - 1) = 1 :=
id                                      └───────┘        └───┘  └┘                       
src                                     └───────┘         └───┘                               
typ                                     └───────┘        └───┘  └┘                       
doc                                      └───────┘
 39  by rw [← units.mk0_val ha, ← @units.coe_one (zmodp p hp), ← units.coe_pow, ← units.ext_iff,
id            └───────────┘ └┘     └───────────┘  └───┘  └┘     └───────────┘    └───────────┘
src     └────┘└───────────┘  └──┘ └───────────┘ └───┘   └───┘└───────────┘└──┘└───────────┘└─
typ     └────┘└───────────┘└┘└──┘ └───────────┘ └───┘└┘└───┘└───────────┘└──┘└───────────┘└─
doc     └────┘               └──┘                       └───┘             └──┘             └─
txt     └────┘               └──┘                       └───┘             └──┘             └─
par     └────┘               └──┘                       └───┘             └──┘             └─
pid       └──┘               └──┘                       └───┘             └──┘             └─
st     └─────────────────────┘└─────────────────────────────┘└───────────────┘└───────────────┘└─
 40      ← card_units_zmodp hp, pow_card_eq_one]
id         └──────────────┘ └┘  └─────────────┘
src  ─────┘└──────────────┘  └┘└─────────────┘└─
typ  ─────┘└──────────────┘└┘└┘└─────────────┘└─
doc  ─────┘                  └┘               └─
txt  ─────┘                  └┘               └─
par  ─────┘                  └┘               └─
pid  ─────┘                  └┘               
st   ────────────────────────┘└───────────────┘
 41  
src  
typ  
doc  
txt  
par  
pid  
st   
 42  lemma euler_criterion_units {x : units (zmodp p hp)} :
id                                    └───┘  └───┘  └┘
src                                   └───┘  └───┘
typ                                   └───┘  └───┘  └┘
 43    (∃ y : units (zmodp p hp), y ^ 2 = x) ↔ x ^ (p / 2) = 1 :=
id           └───┘  └───┘  └┘                  
src          └───┘  └───┘                           
typ          └───┘  └───┘  └┘                  
 44  hp.eq_two_or_odd.elim
id   └┘└────────────┘└───┘
src    └────────────┘└───┘
typ  └┘└────────────┘└───┘
 45    (λ h, by resetI; subst h; revert x; exact dec_trivial)
id                                             └─────────┘
src             └────┘  └────┘   └──────┘  └────┘└─────────┘
typ            └────┘  └────┘  └──────┘  └────┘└─────────┘
doc             └────┘  └────┘   └──────┘  └────┘└─────────┘
txt             └────┘  └────┘   └──────┘  └────┘
par             └────┘  └────┘   └──────┘  └────┘
pid                                   └┘       
st             └───────────────────────────────────────────┘
 46    (λ hp1, let ⟨g, hg⟩ := is_cyclic.exists_generator (units (zmodp p hp)) in
id        └─┘  └─┘    └┘     └────────────────────────┘  └───┘  └───┘  └┘
src                           └────────────────────────┘  └───┘  └───┘
typ       └─┘  └─┘    └┘     └────────────────────────┘  └───┘  └───┘  └┘
 47      let ⟨n, hn⟩ := show x ∈ powers g, from (powers_eq_gpowers g).symm ▸ hg x in
id       └─┘                  └────┘          └───────────────┘   └──┘      
src                             └────┘          └───────────────┘   └──┘  
typ      └─┘                  └────┘          └───────────────┘   └──┘      
doc                              └────┘
 48      ⟨λ ⟨y, hy⟩, by rw [← hy, ← pow_mul, two_mul_odd_div_two hp1,
id                           └┘    └─────┘  └─────────────────┘ └─┘
src                     └────┘  └──┘└─────┘└┘└─────────────────┘   └─
typ                    └────┘└┘└──┘└─────┘└┘└─────────────────┘└─┘└─
doc                     └────┘  └──┘       └┘                      └─
txt                     └────┘  └──┘       └┘                      └─
par                     └────┘  └──┘       └┘                      └─
pid                       └──┘  └──┘       └┘                      └─
st                     └───────┘└─────────┘└───────────────────────┘└─
 49          ← card_units_zmodp hp, pow_card_eq_one],
id             └──────────────┘ └┘  └─────────────┘
src  ─────────┘└──────────────┘  └┘└─────────────┘
typ  ─────────┘└──────────────┘└┘└┘└─────────────┘
doc  ─────────┘                  └┘               
txt  ─────────┘                  └┘               
par  ─────────┘                  └┘               
pid  ─────────┘                  └┘               
st   ────────────────────────────┘└───────────────┘
 50      λ hx, have 2 * (p / 2) ∣ n * (p / 2),
id         └┘                      
src                                  
typ        └┘                      
 51          by rw [two_mul_odd_div_two hp1, ← card_units_zmodp hp, ← order_of_eq_card_of_forall_mem_gpowers hg];
id                  └─────────────────┘ └─┘    └──────────────┘ └┘    └────────────────────────────────────┘ └┘
src             └──┘└─────────────────┘   └──┘└──────────────┘  └──┘└────────────────────────────────────┘  
typ             └──┘└─────────────────┘└─┘└──┘└──────────────┘└┘└──┘└────────────────────────────────────┘└┘
doc             └──┘                      └──┘                  └──┘                                        
txt             └──┘                      └──┘                  └──┘                                        
par             └──┘                      └──┘                  └──┘                                        
pid               └┘                      └──┘                  └──┘                                        
st             └──────────────────────────┘└─────────────────────┘└───────────────────────────────────────────┘└─
 52          exact order_of_dvd_of_pow_eq_one (by rwa [pow_mul, hn]),
id                 └────────────────────────┘          └─────┘  └┘
src          └────┘└────────────────────────┘   └───┘└─────┘└┘  
typ          └────┘└────────────────────────┘   └───┘└─────┘└┘└┘
doc          └────┘                             └───┘       └┘  
txt          └────┘                             └───┘       └┘  
par          └────┘                             └───┘       └┘  
pid                                            └────┘       └┘  └┘
st   ───────────────────────────────────────────┘└───────────┘└──┘
 53        let ⟨m, hm⟩ := dvd_of_mul_dvd_mul_right (nat.div_pos hp.two_le dec_trivial) this in
id         └─┘           └──────────────────────┘  └─────────┘ └┘└─────┘ └─────────┘  └──┘
src                       └──────────────────────┘  └─────────┘   └─────┘ └─────────┘
typ        └─┘           └──────────────────────┘  └─────────┘ └┘└─────┘ └─────────┘  └──┘
doc                                                                       └─────────┘
 54        ⟨g ^ m, by rwa [← pow_mul, mul_comm, ← hm]⟩⟩)
id                          └─────┘  └──────┘    └┘
src                  └─────┘└─────┘└┘└──────┘└──┘  
typ                  └─────┘└─────┘└┘└──────┘└──┘└┘
doc                   └─────┘       └┘        └──┘  
txt                   └─────┘       └┘        └──┘  
par                   └─────┘       └┘        └──┘  
pid                      └──┘       └┘        └──┘  
st                   └─────────────┘└────────┘└────┘
 55  
 56  lemma euler_criterion {a : zmodp p hp} (ha : a ≠ 0) :
id                              └───┘  └┘         
src                             └───┘               
typ                             └───┘  └┘         
 57    (∃ y : zmodp p hp, y ^ 2 = a) ↔ a ^ (p / 2) = 1 :=
id           └───┘  └┘                 
src          └───┘                          
typ          └───┘  └┘                 
 58  ⟨λ ⟨y, hy⟩,
id      
typ     
 59    have hy0 : y ≠ 0, from λ h, by simp [h, _root_.zero_pow (succ_pos 1)] at hy; cc,
id                                          └─────────────┘  └──────┘
src                                  └────┘ └┘└─────────────┘ └──────┘└────────┘  └┘
typ                                 └────┘└┘└─────────────┘ └──────┘└────────┘  └┘
doc                                   └────┘ └┘                        └────────┘  └┘
txt                                   └────┘ └┘                        └────────┘  └┘
par                                   └────┘ └┘                        └────────┘  └┘
pid                                        └┘                        └──┘└───┘
st                                   └───────────────────────────────────────────────┘
 60    by simpa using (units.ext_iff.1 $ (euler_criterion_units hp).1 ⟨units.mk0 _ hy0, show _ = units.mk0 _ ha,
id                     └───────────┘      └───────────────────┘ └┘                 └─┘          └───────┘   └┘
src       └──────────┘ └───────────┘└─┘  └───────────────────┘  └──┘          └─┘   └┘    └─┘└───────┘└─┘  └─
typ       └──────────┘ └───────────┘└─┘  └───────────────────┘└┘└──┘          └─┘└─┘└┘    └─┘└───────┘└─┘└┘└─
doc       └──────────┘              └─┘                         └──┘          └─┘   └┘    └─┘ └───────┘└─┘  └─
txt       └──────────┘              └─┘                         └──┘          └─┘   └┘    └─┘          └─┘  └─
par       └──────────┘              └─┘                         └──┘          └─┘   └┘    └─┘          └─┘  └─
pid            └────┘              └─┘                         └──┘          └─┘   └┘    └─┘          └─┘  └─
st       └───────────────────────────────────────────────────────────────────────────────────────────────────────
 61      by rw [units.ext_iff]; simpa⟩),
id              └───────────┘
src  ──────┘└──┘└───────────┘└───────┘
typ  ──────┘└──┘└───────────┘└───────┘
doc  ──────┘└──┘             └───────┘
txt  ──────┘└──┘             └───────┘
par  ──────┘└──┘             └───────┘
pid  ──────────┘             └────────┘
st   ─────┘└────────────────┘└─────┘└┘
 62  λ h, let ⟨y, hy⟩ := (euler_criterion_units hp).2 (show units.mk0 _ ha ^ (p / 2) = 1, by simpa [units.ext_iff]) in
id       └─┘            └───────────────────┘ └┘         └───────┘   └┘                      └───────────┘
src                       └───────────────────┘            └───────┘                     └─────┘└───────────┘
typ      └─┘            └───────────────────┘ └┘         └───────┘   └┘               └─────┘└───────────┘
doc                                                         └───────┘                        └─────┘             
txt                                                                                          └─────┘             
par                                                                                          └─────┘             
pid                                                                                                            
st                                                                                          └────────────────────┘
 63    ⟨y, by simpa [units.ext_iff] using hy⟩⟩
id                   └───────────┘        └┘
src           └─────┘└───────────┘└──────┘
typ           └─────┘└───────────┘└──────┘└┘
doc           └─────┘             └──────┘
txt           └─────┘             └──────┘
par           └─────┘             └──────┘
pid                             └────┘
st           └─────────────────────────────┘
 64  
 65  lemma exists_pow_two_eq_neg_one_iff_mod_four_ne_three :
 66    (∃ y : zmodp p hp, y ^ 2 = -1) ↔ p % 4 ≠ 3 :=
id           └───┘  └┘              
src          └───┘                     
typ          └───┘  └┘              
 67  have (-1 : zmodp p hp) ≠ 0, from mt neg_eq_zero.1 one_ne_zero,
id             └───┘  └┘           └┘ └─────────┘  └─────────┘
src            └───┘                └┘ └─────────┘  └─────────┘
typ            └───┘  └┘           └┘ └─────────┘  └─────────┘
 68  hp.eq_two_or_odd.elim (λ hp, by resetI; subst hp; exact dec_trivial)
id   └┘└────────────┘└───┘    └┘                   └┘        └─────────┘
src    └────────────┘└───┘           └────┘  └────┘    └────┘└─────────┘
typ  └┘└────────────┘└───┘    └┘     └────┘  └────┘└┘  └────┘└─────────┘
doc                                  └────┘  └────┘    └────┘└─────────┘
txt                                  └────┘  └────┘    └────┘
par                                  └────┘  └────┘    └────┘
pid                                                        
st                                  └──────────────────────────────────┘
 69    (λ hp1, (mod_two_eq_zero_or_one (p / 2)).elim
id        └─┘   └────────────────────┘       └──┘
src             └────────────────────┘        └──┘
typ       └─┘   └────────────────────┘       └──┘
 70      (λ hp2, begin
id          └─┘
typ         └─┘
st               └─────
 71        rw [euler_criterion hp this, neg_one_pow_eq_pow_mod_two, hp2, _root_.pow_zero,
id             └─────────────┘ └┘ └──┘  └────────────────────────┘  └─┘  └─────────────┘
src        └──┘└─────────────┘      └┘└────────────────────────┘└┘   └┘└─────────────┘└─
typ        └──┘└─────────────┘└┘└──┘└┘└────────────────────────┘└┘└─┘└┘└─────────────┘└─
doc        └──┘                     └┘                          └┘   └┘               └─
txt        └──┘                     └┘                          └┘   └┘               └─
par        └──┘                     └┘                          └┘   └┘               └─
pid          └┘                     └┘                          └┘   └┘               └─
st   ────────────────────────────────┘└──────────────────────────┘└───┘└───────────────┘└─
 72          eq_self_iff_true, true_iff],
id           └──────────────┘  └──────┘
src  ───────┘└──────────────┘└┘└──────┘
typ  ───────┘└──────────────┘└┘└──────┘
doc  ───────┘                └┘        
txt  ───────┘                └┘        
par  ───────┘                └┘        
pid  ───────┘                └┘        
st   ───────────────────────┘└────────┘└──
 73        assume h,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────────────┘└─
 74        rw [← nat.mod_mul_right_div_self, show 2 * 2 = 4, from rfl, h] at hp2,
id               └────────────────────────┘                     └─┘  
src        └────┘└────────────────────────┘└┘    └─┘└─┘└───────┘└─┘└┘ └──────┘
typ        └────┘└────────────────────────┘└┘    └─┘└─┘└───────┘└─┘└┘└──────┘
doc        └────┘                          └┘    └─┘ └─┘ └───────┘   └┘ └──────┘
txt        └────┘                          └┘    └─┘ └─┘ └───────┘   └┘ └──────┘
par        └────┘                          └┘    └─┘ └─┘ └───────┘   └┘ └──────┘
pid          └──┘                          └┘    └─┘ └─┘ └───────┘   └┘ └─────┘
st   ─────────────────────────────────────┘└────────────────────────┘└─┘└─────┘└─
 75        exact absurd hp2 dec_trivial,
id               └────┘ └─┘
src        └────┘└────┘   
typ        └────┘└────┘└─┘
doc        └────┘         
txt        └────┘         
par        └────┘         
pid                      
st   ─────────────────────────────────┘└─
 76      end)
st   ──────┘
 77      (λ hp2, begin
id          └─┘
typ         └─┘
st               └─────
 78        rw [euler_criterion hp this, neg_one_pow_eq_pow_mod_two, hp2, _root_.pow_one,
id             └─────────────┘ └┘ └──┘  └────────────────────────┘  └─┘  └────────────┘
src        └──┘└─────────────┘      └┘└────────────────────────┘└┘   └┘└────────────┘└─
typ        └──┘└─────────────┘└┘└──┘└┘└────────────────────────┘└┘└─┘└┘└────────────┘└─
doc        └──┘                     └┘                          └┘   └┘              └─
txt        └──┘                     └┘                          └┘   └┘              └─
par        └──┘                     └┘                          └┘   └┘              └─
pid          └┘                     └┘                          └┘   └┘              └─
st   ────────────────────────────────┘└──────────────────────────┘└───┘└──────────────┘└─
 79          iff_false_intro (zmodp.ne_neg_self hp hp1 one_ne_zero).symm, false_iff,
id           └─────────────┘  └───────────────┘ └┘ └─┘ └─────────┘        └───────┘
src  ───────┘└─────────────┘ └───────────────┘     └─────────┘└──────┘└───────┘└─
typ  ───────┘└─────────────┘ └───────────────┘└┘└─┘└─────────┘└──────┘└───────┘└─
doc  ───────┘                                                 └──────┘         └─
txt  ───────┘                                                 └──────┘         └─
par  ───────┘                                                 └──────┘         └─
pid  ───────┘                                                 └──────┘         └─
st   ─────────────────────────────────────────────────────────────────┘└──────────┘└─
 80          not_not],
id           └─────┘
src  ───────┘└─────┘
typ  ───────┘└─────┘
doc  ───────┘       
txt  ───────┘       
par  ───────┘       
pid  ───────┘       
st   ──────────────┘└──
 81        rw [← nat.mod_mul_right_div_self, show 2 * 2 = 4, from rfl] at hp2,
id               └────────────────────────┘                       └─┘
src        └────┘└────────────────────────┘└┘    └─┘ └─┘ └───────┘└─┘└──────┘
typ        └────┘└────────────────────────┘└┘    └─┘ └─┘ └───────┘└─┘└──────┘
doc        └────┘                          └┘    └─┘ └─┘ └───────┘   └──────┘
txt        └────┘                          └┘    └─┘ └─┘ └───────┘   └──────┘
par        └────┘                          └┘    └─┘ └─┘ └───────┘   └──────┘
pid          └──┘                          └┘    └─┘ └─┘ └───────┘   └─────┘
st   ─────────────────────────────────────┘└────────────────────────┘└─────┘└─
 82        rw [← nat.mod_mul_left_mod _ 2, show 2 * 2 = 4, from rfl] at hp1,
id               └──────────────────┘                           └─┘
src        └────┘└──────────────────┘└────┘    └─┘ └─┘ └───────┘└─┘└──────┘
typ        └────┘└──────────────────┘└────┘    └─┘ └─┘ └───────┘└─┘└──────┘
doc        └────┘                    └────┘    └─┘ └─┘ └───────┘   └──────┘
txt        └────┘                    └────┘    └─┘ └─┘ └───────┘   └──────┘
par        └────┘                    └────┘    └─┘ └─┘ └───────┘   └──────┘
pid          └──┘                    └────┘    └─┘ └─┘ └───────┘   └─────┘
st   ──────────────────────────────────┘└─────────────────────────┘└─────┘└─
 83        have hp4 : p % 4 < 4, from nat.mod_lt _ dec_trivial,
id                                 └────────┘
src        └─────────┘ └─┘└┘  └───┘└────────┘└─┘
typ        └─────────┘└─┘└┘  └───┘└────────┘└─┘
doc        └─────────┘  └─┘ └┘  └───┘          └─┘
txt        └─────────┘  └─┘ └┘  └───┘          └─┘
par        └─────────┘  └─┘ └┘  └───┘          └─┘
pid        └──────┘└─┘  └─┘   └───┘          └─┘
st   ─────────────────────────┘└─────────────────────────────┘└─
 84        revert hp1 hp2, revert hp4,
src        └────────────┘  └────────┘
typ        └────────────┘  └────────┘
doc        └────────────┘  └────────┘
txt        └────────────┘  └────────┘
par        └────────────┘  └────────┘
pid              └──────┘        └──┘
st   ───────────────────┘└──────────┘└─
 85        generalize : p % 4 = k,
id                      
src        └───────────┘  └─┘ 
typ        └───────────┘ └─┘ 
doc        └───────────┘  └─┘ 
txt        └───────────┘  └─┘ 
par        └───────────┘  └─┘ 
pid                    └─┘ 
st   ───────────────────────────┘└─
 86        revert k, exact dec_trivial
src        └──────┘  └────┘           
typ        └──────┘  └────┘           
doc        └──────┘  └────┘           
txt        └──────┘  └────┘           
par        └──────┘  └────┘           
pid              └┘                  
st   ─────────────┘└───────────────────
 87      end))
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
 88  
 89  lemma pow_div_two_eq_neg_one_or_one {a : zmodp p hp} (ha : a ≠ 0) : a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1 :=
id                                            └───┘  └┘                                    
src                                           └───┘                                              
typ                                           └───┘  └┘                                    
 90  hp.eq_two_or_odd.elim
id   └┘└────────────┘└───┘
src    └────────────┘└───┘
typ  └┘└────────────┘└───┘
 91    (λ h, by revert a ha; resetI; subst h; exact dec_trivial)
id                                                └─────────┘
src             └─────────┘  └────┘  └────┘   └────┘└─────────┘
typ            └─────────┘  └────┘  └────┘  └────┘└─────────┘
doc             └─────────┘  └────┘  └────┘   └────┘└─────────┘
txt             └─────────┘  └────┘  └────┘   └────┘
par             └─────────┘  └────┘  └────┘   └────┘
pid                   └───┘                       
st             └──────────────────────────────────────────────┘
 92    (λ hp1, by rw [← mul_self_eq_one_iff, ← _root_.pow_add, ← two_mul, two_mul_odd_div_two hp1];
id        └─┘           └─────────────────┘    └────────────┘    └─────┘  └─────────────────┘ └─┘
src               └────┘└─────────────────┘└──┘└────────────┘└──┘└─────┘└┘└─────────────────┘   
typ       └─┘     └────┘└─────────────────┘└──┘└────────────┘└──┘└─────┘└┘└─────────────────┘└─┘
doc               └────┘                   └──┘              └──┘       └┘                      
txt               └────┘                   └──┘              └──┘       └┘                      
par               └────┘                   └──┘              └──┘       └┘                      
pid                 └──┘                   └──┘              └──┘       └┘                      
st               └────────────────────────┘└────────────────┘└─────────┘└───────────────────────┘└─
 93      exact fermat_little hp ha)
id             └───────────┘ └┘ └┘
src      └────┘└───────────┘  
typ      └────┘└───────────┘└┘└┘
doc      └────┘               
txt      └────┘               
par      └────┘               
pid                          
st   ────────────────────────────┘
 94  
 95  @[simp] lemma wilsons_lemma {p : ℕ} (hp : nat.prime p) : (fact (p - 1) : zmodp p hp) = -1 :=
id                                            └───────┘      └──┘         └───┘  └┘   
src                                           └───────┘       └──┘          └───┘        
typ                                           └───────┘      └──┘         └───┘  └┘   
doc    └──┘                                    └───────┘       └──┘
 96  begin
st   └─────
 97    rw [← finset.prod_Ico_id_eq_fact, ← @units.coe_one (zmodp p hp), ← units.coe_neg,
id           └────────────────────────┘     └───────────┘  └───┘  └┘     └───────────┘
src    └────┘└────────────────────────┘└──┘ └───────────┘ └───┘   └───┘└───────────┘└─
typ    └────┘└────────────────────────┘└──┘ └───────────┘ └───┘└┘└───┘└───────────┘└─
doc    └────┘                          └──┘                       └───┘└───────────┘└─
txt    └────┘                          └──┘                       └───┘             └─
par    └────┘                          └──┘                       └───┘             └─
pid      └──┘                          └──┘                       └───┘             └─
st   ─────────────────────────────────┘└─────────────────────────────┘└───────────────┘└─
 98      ← @prod_univ_units_id_eq_neg_one (zmodp p hp),
id          └───────────────────────────┘  └───┘  └┘
src  ─────┘ └───────────────────────────┘ └───┘   └──
typ  ─────┘ └───────────────────────────┘ └───┘└┘└──
doc  ─────┘                                       └──
txt  ─────┘                                       └──
par  ─────┘                                       └──
pid  ─────┘                                       └──
st   ────────────────────────────────────────────────┘└─
 99      ← prod_hom _ (coe : units (zmodp p hp) → zmodp p hp),
id         └──────┘    └─┘   └───┘                └───┘  └┘
src  ─────┘└──────┘└─┘ └─┘└─┘└───┘         └┘ └───┘   └──
typ  ─────┘└──────┘└─┘ └─┘└─┘└───┘         └┘ └───┘└┘└──
doc  ─────┘        └─┘    └─┘              └┘         └──
txt  ─────┘        └─┘    └─┘              └┘         └──
par  ─────┘        └─┘    └─┘              └┘         └──
pid  ─────┘        └─┘    └─┘              └┘         └──
st   ───────────────────────────────────────────────────────┘└─
100      ← prod_hom _ (coe : ℕ → zmodp p hp)],
id         └──────┘    └─┘       └───┘  └┘
src  ─────┘└──────┘└─┘ └─┘└─┘  └───┘   └┘
typ  ─────┘└──────┘└─┘ └─┘└─┘  └───┘└┘└┘
doc  ─────┘        └─┘    └─┘          └┘
txt  ─────┘        └─┘    └─┘          └┘
par  ─────┘        └─┘    └─┘          └┘
pid  ─────┘        └─┘    └─┘          └┘
st   ──────────────────────────────────────┘└──
101    exact eq.symm (prod_bij
id           └─────┘  └──────┘
src    └────┘└─────┘ └──────┘
typ    └────┘└─────┘ └──────┘
doc    └────┘                
txt    └────┘                
par    └────┘                
pid                         
st   ──────────────────────────
102      (λ a _, (a : zmodp p hp).1)
src  ───┘  └────┘  └─┘        └────
typ  ───┘  └────┘  └─┘        └────
doc  ───┘  └────┘  └─┘        └────
txt  ───┘  └────┘  └─┘        └────
par  ───┘  └────┘  └─┘        └────
pid  ───┘  └────┘  └─┘        └────
st   ────────────────────────────────
103      (λ a ha, Ico.mem.2 ⟨nat.pos_of_ne_zero
id                └─────┘    └────────────────┘
src  ───┘  └─────┘└─────┘└─┘ └────────────────┘
typ  ───┘  └─────┘└─────┘└─┘ └────────────────┘
doc  ───┘  └─────┘       └─┘                   
txt  ───┘  └─────┘       └─┘                   
par  ───┘  └─────┘       └─┘                   
pid  ───┘  └─────┘       └─┘                   
st   ───────────────────────────────────────────
104          (λ h, units.coe_ne_zero a (fin.eq_of_veq h)),
id                 └───────────────┘
src  ───────┘  └──┘└───────────────┘                └───
typ  ───────┘  └──┘└───────────────┘                └───
doc  ───────┘  └──┘└───────────────┘                └───
txt  ───────┘  └──┘                                 └───
par  ───────┘  └──┘                                 └───
pid  ───────┘  └──┘                                 └───
st   ──────────────────────────────────────────────────────
105        by rw [← succ_sub hp.pos, succ_sub_one]; exact (a : zmodp p hp).2⟩)
id                  └──────┘ └────┘  └──────────┘             └───┘  └┘
src  ─────┘  └────┘└──────┘└────┘└┘└──────────┘└──────┘  └─┘└───┘   └─────
typ  ─────┘  └────┘└──────┘└────┘└┘└──────────┘└──────┘ └─┘└───┘└┘└─────
doc  ─────┘  └────┘              └┘            └──────┘  └─┘        └─────
txt  ─────┘  └────┘              └┘            └──────┘  └─┘        └─────
par  ─────┘  └────┘              └┘            └──────┘  └─┘        └─────
pid  ─────┘  └─────┘              └┘            └───────┘  └─┘        └─────
st   ───────┘└────────────────────┘└────────────┘└────────────────────────┘└──
106      (λ a _, by simp) (λ _ _ _ _, units.ext_iff.2 ∘ fin.eq_of_veq)
id                                    └───────────┘    └───────────┘
src  ───┘  └────┘  └──┘└┘  └────────┘└───────────┘└─┘└───────────┘└─
typ  ───┘  └────┘  └──┘└┘  └────────┘└───────────┘└─┘└───────────┘└─
doc  ───┘  └────┘  └──┘└┘  └────────┘             └─┘              └─
txt  ───┘  └────┘  └──┘└┘  └────────┘             └─┘              └─
par  ───┘  └────┘  └──┘└┘  └────────┘             └─┘              └─
pid  ───┘  └────┘  └─────┘  └────────┘             └─┘              └─
st   ─────────────┘└───┘└──────────────────────────────────────────────
107      (λ b hb,
src  ───┘  └──────
typ  ───┘  └──────
doc  ───┘  └──────
txt  ───┘  └──────
par  ───┘  └──────
pid  ───┘  └──────
st   ─────────────
108        have b ≠ 0 ∧ b < p, by rwa [Ico.mem, nat.succ_le_iff, ← succ_sub hp.pos,
id                                  └─────┘  └─────────────┘    └──────┘ └────┘
src  ─────┘    └─┘└─┘  └───┘└───┘└─────┘└┘└─────────────┘└──┘└──────┘└────┘└─
typ  ─────┘    └─┘└─┘  └───┘└───┘└─────┘└┘└─────────────┘└──┘└──────┘└────┘└─
doc  ─────┘    └─┘ └─┘    └───┘└───┘       └┘               └──┘              └─
txt  ─────┘    └─┘ └─┘    └───┘└───┘       └┘               └──┘              └─
par  ─────┘    └─┘ └─┘    └───┘└───┘       └┘               └──┘              └─
pid  ─────┘    └─┘ └─┘    └────────┘       └┘               └──┘              └─
st   ───────────────────────────┘└───────────┘└───────────────┘└─────────────────┘└─
109          succ_sub_one, nat.pos_iff_ne_zero] at hb,
id           └──────────┘  └─────────────────┘
src  ───────┘└──────────┘└┘└─────────────────┘└─────┘└─
typ  ───────┘└──────────┘└┘└─────────────────┘└─────┘└─
doc  ───────┘            └┘                   └─────┘└─
txt  ───────┘            └┘                   └─────┘└─
par  ───────┘            └┘                   └─────┘└─
pid  ───────┘            └┘                   └────────
st   ───────────────────┘└───────────────────┘└────┘└─
110        ⟨units.mk0 _ (show (b : zmodp p hp) ≠ 0, from fin.ne_of_vne $
id          └───────┘              └───┘  └┘           └───────────┘
src  ─────┘ └───────┘└─┘       └─┘└───┘   └┘ └───────┘└───────────┘ 
typ  ─────┘ └───────┘└─┘       └─┘└───┘└┘└┘└───────┘└───────────┘ 
doc  ─────┘ └───────┘└─┘       └─┘        └┘ └───────┘              
txt  ─────┘          └─┘       └─┘        └┘ └───────┘              
par  ─────┘          └─┘       └─┘        └┘ └───────┘              
pid  ─────┘          └─┘       └─┘        └┘ └───────┘              
st   ────────────────────────────────────────────────────────────────────
111          by rw [zmod.val_cast_nat, ← @nat.cast_zero (zmodp p hp), zmod.val_cast_nat];
id                  └───────────────┘     └───────────┘  └───┘  └┘   └───────────────┘
src  ───────┘  └──┘└───────────────┘└──┘ └───────────┘ └───┘   └─┘└───────────────┘└─
typ  ───────┘  └──┘└───────────────┘└──┘ └───────────┘ └───┘└┘└─┘└───────────────┘└─
doc  ───────┘  └──┘                 └──┘                       └─┘                 └─
txt  ───────┘  └──┘                 └──┘                       └─┘                 └─
par  ───────┘  └──┘                 └──┘                       └─┘                 └─
pid  ───────┘  └───┘                 └──┘                       └─┘                 └──
st   ─────────┘└────────────────────┘└─────────────────────────────┘└─────────────────┘└─
112          simp [mod_eq_of_lt this.2, this.1]), mem_univ _,
id                 └──────────┘ └──┘    └──┘      └──────┘
src  ───────┘└────┘└──────────┘    └──┘    └─┘└─┘└──────┘└───
typ  ───────┘└────┘└──────────┘└──┘└──┘└──┘└─┘└─┘└──────┘└───
doc  ───────┘└────┘                └──┘    └─┘└─┘        └───
txt  ───────┘└────┘                └──┘    └─┘└─┘        └───
par  ───────┘└────┘                └──┘    └─┘└─┘        └───
pid  ─────────────┘                └──┘    └────┘        └───
st   ─────────────────────────────────────────┘└──────────────
113        by simp [val_cast_of_lt hp this.2]⟩))
id                  └────────────┘ └┘ └──┘
src  ─────┘  └────┘└────────────┘      └─┘└──┘
typ  ─────┘  └────┘└────────────┘└┘└──┘└─┘└──┘
doc  ─────┘  └────┘                    └─┘└──┘
txt  ─────┘  └────┘                    └─┘└──┘
par  ─────┘  └────┘                    └─┘└──┘
pid  ─────┘  └─────┘                    └────┘
st   ───────┘└──────────────────────────────┘└──┘
114  end
st   └─┘
115  
116  @[simp] lemma prod_Ico_one_prime {p : ℕ} (hp : nat.prime p) :
id                                                 └───────┘ 
src                                                └───────┘
typ                                                └───────┘ 
doc    └──┘                                         └───────┘
117    (Ico 1 p).prod (λ x, (x : zmodp p hp)) = -1 :=
id      └─┘    └──┘           └───┘  └┘    
src     └─┘     └──┘             └───┘         
typ     └─┘    └──┘           └───┘  └┘    
doc     └─┘     └──┘
118  by conv in (Ico 1 p) { rw [← succ_sub_one p, succ_sub hp.pos] };
id               └─┘             └──────────┘   └──────┘ └────┘
src     └──────┘ └─┘└─┘ └──┘└────┘└──────────┘ └┘└──────┘└────┘└┘
typ     └──────┘ └─┘└─┘└──┘└────┘└──────────┘└┘└──────┘└────┘└┘
doc              └─┘
txt     └──────┘    └─┘ └──┘└────┘             └┘              └┘
par     └──────┘    └─┘ └──┘└────┘             └┘              └┘
pid         └─┘    └─┘ └───────┘             └┘              └─┘
st     └──────────────────┘└───────────────────┘└───────────────┘ └┘
119    rw [prod_hom _ (coe : ℕ → zmodp p hp),
id         └──────┘    └─┘       └───┘  └┘
src    └──┘└──────┘└─┘ └─┘└─┘  └───┘   └──
typ    └──┘└──────┘└─┘ └─┘└─┘  └───┘└┘└──
doc    └──┘        └─┘    └─┘          └──
txt    └──┘        └─┘    └─┘          └──
par    └──┘        └─┘    └─┘          └──
pid      └┘        └─┘    └─┘          └──
st   ─────┘└───────────────────────────────┘└─
120      finset.prod_Ico_id_eq_fact, wilsons_lemma]
id       └────────────────────────┘  └───────────┘
src  ───┘└────────────────────────┘└┘└───────────┘└─
typ  ───┘└────────────────────────┘└┘└───────────┘└─
doc  ───┘                          └┘             └─
txt  ───┘                          └┘             └─
par  ───┘                          └┘             └─
pid  ───┘                          └┘             
st   ─────────────────────────────┘└─────────────┘
121  
src  
typ  
doc  
txt  
par  
pid  
st   
122  end zmodp
123  
124  /-- The image of the map sending a non zero natural number `x ≤ p / 2` to the absolute value
125    of the element of interger in the interval `(-p/2, p/2]` congruent to `a * x` mod p is the set
126    of non zero natural numbers `x` such that `x ≤ p / 2` -/
127  lemma Ico_map_val_min_abs_nat_abs_eq_Ico_map_id
128    {p : ℕ} (hp : p.prime) (a : zmodp p hp) (hpa : a ≠ 0) :
id                  └────┘       └───┘  └┘          
src                  └────┘       └───┘                
typ                 └────┘       └───┘  └┘          
doc                   └────┘
129    (Ico 1 (p / 2).succ).1.map (λ x, (a * x).val_min_abs.nat_abs) =
id      └─┘        └──┘   └─┘           └─────────┘ └─────┘   
src     └─┘         └──┘   └─┘              └─────────┘ └─────┘   
typ     └─┘        └──┘   └─┘           └─────────┘ └─────┘   
doc     └─┘                  └─┘               └─────────┘
130    (Ico 1 (p / 2).succ).1.map (λ a, a) :=
id      └─┘        └──┘   └─┘       
src     └─┘         └──┘   └─┘
typ     └─┘        └──┘   └─┘       
doc     └─┘                  └─┘
131  have he : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2,
id                     └─┘        └──┘            
src                      └─┘         └──┘               
typ                    └─┘        └──┘            
doc                       └─┘
132    by simp [nat.lt_succ_iff, nat.succ_le_iff, nat.pos_iff_ne_zero] {contextual := tt},
id              └─────────────┘  └─────────────┘  └─────────────────┘                 └┘
src       └────┘└─────────────┘└┘└─────────────┘└┘└─────────────────┘└┘ └────────────┘└┘
typ       └────┘└─────────────┘└┘└─────────────┘└┘└─────────────────┘└┘ └────────────┘└┘
doc       └────┘               └┘               └┘                   └┘ └────────────┘  
txt       └────┘               └┘               └┘                   └┘ └────────────┘  
par       └────┘               └┘               └┘                   └┘ └────────────┘  
pid                          └┘               └┘                    └────────────┘  
st       └──────────────────────────────────────────────────────────────────────────────┘
133  have hep : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x < p,
id                      └─┘        └──┘      
src                       └─┘         └──┘      
typ                     └─┘        └──┘      
doc                        └─┘
134    from λ x hx, lt_of_le_of_lt (he hx).2 (nat.div_lt_self hp.pos dec_trivial),
id             └┘  └────────────┘  └┘ └┘    └─────────────┘ └┘└──┘ └─────────┘
src                 └────────────┘           └─────────────┘   └──┘ └─────────┘
typ            └┘  └────────────┘  └┘ └┘    └─────────────┘ └┘└──┘ └─────────┘
doc                                                                  └─────────┘
135  have hpe : ∀ {x}, x ∈ Ico 1 (p / 2).succ → ¬ p ∣ x,
id                      └─┘        └──┘       
src                       └─┘         └──┘       
typ                     └─┘        └──┘       
doc                        └─┘
136    from λ x hx hpx, not_lt_of_ge (le_of_dvd (nat.pos_of_ne_zero (he hx).1) hpx) (hep hx),
id             └┘ └─┘  └──────────┘  └───────┘  └────────────────┘  └┘ └┘    └─┘   └─┘ └┘
src                     └──────────┘  └───────┘  └────────────────┘        
typ            └┘ └─┘  └──────────┘  └───────┘  └────────────────┘  └┘ └┘    └─┘   └─┘ └┘
137  have hsurj : ∀ b : ℕ , b ∈ Ico 1 (p / 2).succ →
id                           └─┘        └──┘
src                           └─┘         └──┘
typ                          └─┘        └──┘
doc                             └─┘
138      ∃ x ∈ Ico 1 (p / 2).succ,
id           └─┘        └──┘ 
src           └─┘         └──┘ 
typ          └─┘        └──┘ 
doc            └─┘
139        b = (a * x : zmodp p hp).val_min_abs.nat_abs,
id                 └───┘  └┘ └─────────┘ └─────┘
src                   └───┘      └─────────┘ └─────┘
typ                └───┘  └┘ └─────────┘ └─────┘
doc                                └─────────┘
140    from λ b hb, ⟨(b / a : zmodp p hp).val_min_abs.nat_abs,
id             └┘         └───┘  └┘ └─────────┘ └─────┘
src                          └───┘      └─────────┘ └─────┘
typ            └┘         └───┘  └┘ └─────────┘ └─────┘
doc                                      └─────────┘
141      Ico.mem.2 ⟨nat.pos_of_ne_zero $
id       └─────┘   └────────────────┘
src      └─────┘   └────────────────┘
typ      └─────┘   └────────────────┘
142          by simp [div_eq_mul_inv, hpa, zmodp.eq_zero_iff_dvd_nat hp b, hpe hb],
id                    └────────────┘  └─┘  └───────────────────────┘ └┘   └─┘ └┘
src             └────┘└────────────┘└┘   └┘└───────────────────────┘   └┘     
typ             └────┘└────────────┘└┘└─┘└┘└───────────────────────┘└┘└┘└─┘└┘
doc             └────┘              └┘   └┘                            └┘     
txt             └────┘              └┘   └┘                            └┘     
par             └────┘              └┘   └┘                            └┘     
pid                               └┘   └┘                            └┘     
st             └─────────────────────────────────────────────────────────────────┘
143        nat.lt_succ_of_le $ zmodp.nat_abs_val_min_abs_le _⟩,
id         └───────────────┘   └──────────────────────────┘
src        └───────────────┘   └──────────────────────────┘
typ        └───────────────┘   └──────────────────────────┘
144      begin
st       └─────
145        rw [zmodp.cast_nat_abs_val_min_abs],
id             └────────────────────────────┘
src        └──┘└────────────────────────────┘
typ        └──┘└────────────────────────────┘
doc        └──┘                              
txt        └──┘                              
par        └──┘                              
pid          └┘                              
st   ───────────────────────────────────────┘└──
146        split_ifs,
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
st   ──────────────┘└─
147        { erw [mul_div_cancel' _ hpa, zmodp.val_min_abs, zmod.val_min_abs,
id                └─────────────┘   └─┘  └───────────────┘  └──────────────┘
src          └───┘└─────────────┘└─┘   └┘└───────────────┘└┘└──────────────┘└─
typ          └───┘└─────────────┘└─┘└─┘└┘└───────────────┘└┘└──────────────┘└─
doc          └───┘               └─┘   └┘└───────────────┘└┘└──────────────┘└─
txt          └───┘               └─┘   └┘                 └┘                └─
par          └───┘               └─┘   └┘                 └┘                └─
pid             └┘               └─┘   └┘                 └┘                └─
st   ───────┘└────────────────────────┘└─────────────────┘└────────────────┘└─
148            zmodp.val_cast_of_lt hp (hep hb), if_pos (le_of_lt_succ (Ico.mem.1 hb).2),
id             └──────────────────┘ └┘  └─┘ └┘   └────┘  └───────────┘  └─────┘   └┘
src  ─────────┘└──────────────────┘        └─┘└────┘ └───────────┘ └─────┘└─┘  └─────
typ  ─────────┘└──────────────────┘└┘ └─┘└┘└─┘└────┘ └───────────┘ └─────┘└─┘└┘└─────
doc  ─────────┘                            └─┘                            └─┘  └─────
txt  ─────────┘                            └─┘                            └─┘  └─────
par  ─────────┘                            └─┘                            └─┘  └─────
pid  ─────────┘                            └─┘                            └─┘  └─────
st   ─────────────────────────────────────────┘└───────────────────────────────────────┘└─
149            int.nat_abs_of_nat], },
id             └────────────────┘
src  ─────────┘└────────────────┘
typ  ─────────┘└────────────────┘
doc  ─────────┘                  
txt  ─────────┘                  
par  ─────────┘                  
pid  ─────────┘                  
st   ───────────────────────────┘└───┘
150        { erw [mul_neg_eq_neg_mul_symm, mul_div_cancel' _ hpa, zmod.nat_abs_val_min_abs_neg,
id                └─────────────────────┘  └─────────────┘   └─┘  └──────────────────────────┘
src          └───┘└─────────────────────┘└┘└─────────────┘└─┘   └┘└──────────────────────────┘└─
typ          └───┘└─────────────────────┘└┘└─────────────┘└─┘└─┘└┘└──────────────────────────┘└─
doc          └───┘                       └┘               └─┘   └┘                            └─
txt          └───┘                       └┘               └─┘   └┘                            └─
par          └───┘                       └┘               └─┘   └┘                            └─
pid             └┘                       └┘               └─┘   └┘                            └─
st   ───────────────────────────────────┘└─────────────────────┘└────────────────────────────┘└─
151            zmod.val_min_abs, zmodp.val_cast_of_lt hp (hep hb),
id             └──────────────┘  └──────────────────┘ └┘  └─┘ └┘
src  ─────────┘└──────────────┘└┘└──────────────────┘        └──
typ  ─────────┘└──────────────┘└┘└──────────────────┘└┘ └─┘└┘└──
doc  ─────────┘└──────────────┘└┘                            └──
txt  ─────────┘                └┘                            └──
par  ─────────┘                └┘                            └──
pid  ─────────┘                └┘                            └──
st   ─────────────────────────┘└────────────────────────────────┘└─
152            if_pos (le_of_lt_succ (Ico.mem.1 hb).2), int.nat_abs_of_nat] },
id             └────┘  └───────────┘  └─────┘   └┘      └────────────────┘
src  ─────────┘└────┘ └───────────┘ └─────┘└─┘  └────┘└────────────────┘└┘
typ  ─────────┘└────┘ └───────────┘ └─────┘└─┘└┘└────┘└────────────────┘└┘
doc  ─────────┘                            └─┘  └────┘                  └┘
txt  ─────────┘                            └─┘  └────┘                  └┘
par  ─────────┘                            └─┘  └────┘                  └┘
pid  ─────────┘                            └─┘  └────┘                  
st   ────────────────────────────────────────────────┘└──────────────────┘└──
153      end⟩,
st   ──────┘
154    have hmem : ∀ x : ℕ, x ∈ Ico 1 (p / 2).succ →
id                           └─┘        └──┘
src                           └─┘         └──┘
typ                          └─┘        └──┘
doc                             └─┘
155      (a * x : zmodp p hp).val_min_abs.nat_abs ∈ Ico 1 (p / 2).succ,
id             └───┘  └┘ └─────────┘ └─────┘   └─┘        └──┘
src              └───┘      └─────────┘ └─────┘   └─┘         └──┘
typ            └───┘  └┘ └─────────┘ └─────┘   └─┘        └──┘
doc                          └─────────┘            └─┘
156    from λ x hx, by simp [hpa, zmodp.eq_zero_iff_dvd_nat hp x, hpe hx, lt_succ_iff, succ_le_iff,
id             └┘           └─┘  └───────────────────────┘ └┘   └─┘ └┘  └─────────┘  └─────────┘
src                    └────┘   └┘└───────────────────────┘   └┘     └┘└─────────┘└┘└─────────┘└─
typ            └┘     └────┘└─┘└┘└───────────────────────┘└┘└┘└─┘└┘└┘└─────────┘└┘└─────────┘└─
doc                    └────┘   └┘                            └┘     └┘           └┘           └─
txt                    └────┘   └┘                            └┘     └┘           └┘           └─
par                    └────┘   └┘                            └┘     └┘           └┘           └─
pid                           └┘                            └┘     └┘           └┘           └─
st                    └─────────────────────────────────────────────────────────────────────────────
157          nat.pos_iff_ne_zero, zmodp.nat_abs_val_min_abs_le _],
id           └─────────────────┘  └──────────────────────────┘
src  ───────┘└─────────────────┘└┘└──────────────────────────┘└─┘
typ  ───────┘└─────────────────┘└┘└──────────────────────────┘└─┘
doc  ───────┘                   └┘                            └─┘
txt  ───────┘                   └┘                            └─┘
par  ───────┘                   └┘                            └─┘
pid  ───────┘                   └┘                            └─┘
st   ───────────────────────────────────────────────────────────┘
158  multiset.map_eq_map_of_bij_of_nodup _ _ (finset.nodup _) (finset.nodup _)
id   └─────────────────────────────────┘      └──────────┘     └──────────┘
src  └─────────────────────────────────┘      └──────────┘     └──────────┘
typ  └─────────────────────────────────┘      └──────────┘     └──────────┘
159    (λ x _, (a * x : zmodp p hp).val_min_abs.nat_abs) hmem (λ _ _, rfl)
id                 └───┘  └┘ └─────────┘ └─────┘   └──┘       └─┘
src                    └───┘      └─────────┘ └─────┘                └─┘
typ                └───┘  └┘ └─────────┘ └─────┘   └──┘       └─┘
doc                                └─────────┘
160    (inj_on_of_surj_on_of_card_le _ hmem hsurj (le_refl _)) hsurj
id      └──────────────────────────┘   └──┘ └───┘  └─────┘     └───┘
src     └──────────────────────────┘               └─────┘
typ     └──────────────────────────┘   └──┘ └───┘  └─────┘     └───┘
161  
162  private lemma gauss_lemma_aux₁ {p : ℕ} (hp : p.prime) (hp2 : p % 2 = 1) {a : ℕ}
id                                               └────┘                      
src                                               └────┘                       
typ                                              └────┘                      
doc                                                └────┘
163    (hpa : (a : zmodp p hp) ≠ 0) :
id                └───┘  └┘  
src                └───┘       
typ               └───┘  └┘  
164    (a^(p / 2) * (p / 2).fact : zmodp p hp) =
id                  └──┘    └───┘  └┘  
src                    └──┘    └───┘       
typ                 └──┘    └───┘  └┘  
doc                        └──┘
165    (-1)^((Ico 1 (p / 2).succ).filter
id          └─┘        └──┘  └────┘
src         └─┘         └──┘  └────┘
typ         └─┘        └──┘  └────┘
doc           └─┘                └────┘
166      (λ x : ℕ, ¬(a * x : zmodp p hp).val ≤ p / 2)).card * (p / 2).fact :=
id                      └───┘  └┘ └─┘        └──┘        └──┘
src                       └───┘      └─┘         └──┘         └──┘
typ                     └───┘  └┘ └─┘        └──┘        └──┘
doc                                                   └──┘           └──┘
167  calc (a ^ (p / 2) * (p / 2).fact : zmodp p hp) =
id                       └──┘    └───┘  └┘
src                         └──┘    └───┘
typ                      └──┘    └───┘  └┘
doc                             └──┘
168      (Ico 1 (p / 2).succ).prod (λ x, a * x) :
id        └─┘        └──┘  └──┘         
src       └─┘         └──┘  └──┘          
typ       └─┘        └──┘  └──┘         
doc       └─┘                └──┘
169    by rw [prod_mul_distrib, ← prod_nat_cast, ← prod_nat_cast, prod_Ico_id_eq_fact,
id            └──────────────┘    └───────────┘    └───────────┘  └─────────────────┘
src       └──┘└──────────────┘└──┘└───────────┘└──┘└───────────┘└┘└─────────────────┘└─
typ       └──┘└──────────────┘└──┘└───────────┘└──┘└───────────┘└┘└─────────────────┘└─
doc       └──┘                └──┘             └──┘             └┘                   └─
txt       └──┘                └──┘             └──┘             └┘                   └─
par       └──┘                └──┘             └──┘             └┘                   └─
pid         └┘                └──┘             └──┘             └┘                   └─
st       └───────────────────┘└───────────────┘└───────────────┘└───────────────────┘└─
170        prod_const, Ico.card, succ_sub_one]; simp
id         └────────┘  └──────┘  └──────────┘
src  ─────┘└────────┘└┘└──────┘└┘└──────────┘  └───┘
typ  ─────┘└────────┘└┘└──────┘└┘└──────────┘  └───┘
doc  ─────┘          └┘        └┘              └───┘
txt  ─────┘          └┘        └┘              └───┘
par  ─────┘          └┘        └┘              └───┘
pid  ─────┘          └┘        └┘                  
st   ───────────────┘└────────┘└────────────┘└─────┘
171  ... = (Ico 1 (p / 2).succ).prod (λ x, (a * x : zmodp p hp).val) : by simp
id          └─┘        └──┘  └──┘             └───┘  └┘ └─┘
src         └─┘         └──┘  └──┘                └───┘      └─┘        └───┘
typ         └─┘        └──┘  └──┘             └───┘  └┘ └─┘        └───┘
doc         └─┘                └──┘                                       └───┘
txt                                                                       └───┘
par                                                                       └───┘
pid                                                                           
st                                                                       └────┘
172  ... = (Ico 1 (p / 2).succ).prod
id          └─┘        └──┘  └──┘
src         └─┘         └──┘  └──┘
typ         └─┘        └──┘  └──┘
doc         └─┘                └──┘
173      (λ x, (if (a * x : zmodp p hp).val ≤ p / 2 then 1 else -1) *
id                      └───┘  └┘ └─┘                      
src                        └───┘      └─┘                       
typ                     └───┘  └┘ └─┘                      
174        (a * x : zmodp p hp).val_min_abs.nat_abs) :
id               └───┘  └┘ └─────────┘ └─────┘
src                └───┘      └─────────┘ └─────┘
typ              └───┘  └┘ └─────────┘ └─────┘
doc                            └─────────┘
175    prod_congr rfl $ λ _ _, begin
id     └────────┘ └─┘      
src    └────────┘ └─┘
typ    └────────┘ └─┘      
st                             └─────
176      simp only [zmodp.cast_nat_abs_val_min_abs],
id                  └────────────────────────────┘
src      └─────────┘└────────────────────────────┘
typ      └─────────┘└────────────────────────────┘
doc      └─────────┘                              
txt      └─────────┘                              
par      └─────────┘                              
pid          └──┘└┘                              
st   ─────────────────────────────────────────────┘└─
177      split_ifs; simp
src      └───────┘  └────
typ      └───────┘  └────
doc      └───────┘  └────
txt      └───────┘  └────
par      └───────┘  └────
pid                     
st   ────────────────────
178    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
179  ... = (-1)^((Ico 1 (p / 2).succ).filter
id              └─┘        └──┘  └────┘
src             └─┘         └──┘  └────┘
typ             └─┘        └──┘  └────┘
doc               └─┘                └────┘
180        (λ x : ℕ, ¬(a * x : zmodp p hp).val ≤ p / 2)).card *
id                        └───┘  └┘ └─┘        └──┘  
src                         └───┘      └─┘         └──┘  
typ                       └───┘  └┘ └─┘        └──┘  
doc                                                     └──┘
181      (Ico 1 (p / 2).succ).prod (λ x, (a * x : zmodp p hp).val_min_abs.nat_abs) :
id        └─┘        └──┘  └──┘             └───┘  └┘ └─────────┘ └─────┘
src       └─┘         └──┘  └──┘                └───┘      └─────────┘ └─────┘
typ       └─┘        └──┘  └──┘             └───┘  └┘ └─────────┘ └─────┘
doc       └─┘                └──┘                            └─────────┘
182    have (Ico 1 (p / 2).succ).prod
id           └─┘        └──┘  └──┘
src          └─┘         └──┘  └──┘
typ          └─┘        └──┘  └──┘
doc          └─┘                └──┘
183          (λ x, if (a * x : zmodp p hp).val ≤ p / 2 then (1 : zmodp p hp) else -1) =
id                         └───┘  └┘ └─┘                 └───┘  └┘          
src                           └───┘      └─┘                  └───┘               
typ                        └───┘  └┘ └─┘                 └───┘  └┘          
184        ((Ico 1 (p / 2).succ).filter
id           └─┘        └──┘  └────┘
src          └─┘         └──┘  └────┘
typ          └─┘        └──┘  └────┘
doc          └─┘                └────┘
185          (λ x : ℕ, ¬(a * x : zmodp p hp).val ≤ p / 2)).prod (λ _, -1),
id                          └───┘  └┘ └─┘        └──┘       
src                           └───┘      └─┘         └──┘        
typ                         └───┘  └┘ └─┘        └──┘       
doc                                                       └──┘
186      from prod_bij_ne_one (λ x _ _, x)
id            └─────────────┘        
src           └─────────────┘
typ           └─────────────┘        
187        (λ x, by split_ifs; simp * at * {contextual := tt})
id                                                       └┘
src                 └───────┘  └──────────┘ └────────────┘└┘
typ                └───────┘  └──────────┘ └────────────┘└┘
doc                 └───────┘  └──────────┘ └────────────┘  
txt                 └───────┘  └──────────┘ └────────────┘  
par                 └───────┘  └──────────┘ └────────────┘  
pid                                └──┘ └────────────┘  
st                 └────────────────────────────────────────┘
188        (λ _ _ _ _ _ _, id)
id                   └┘
src                        └┘
typ                  └┘
189        (λ b h _, ⟨b, by simp [-not_le, *] at *⟩)
id                 
src                         └────────────────────┘
typ                     └────────────────────┘
doc                         └────────────────────┘
txt                         └────────────────────┘
par                         └────────────────────┘
pid                             └──────────┘└──┘
st                         └─────────────────────┘
190        (by intros; split_ifs at *; simp * at *),
src            └────┘  └────────────┘  └─────────┘
typ            └────┘  └────────────┘  └─────────┘
doc            └────┘  └────────────┘  └─────────┘
txt            └────┘  └────────────┘  └─────────┘
par            └────┘  └────────────┘  └─────────┘
pid                             └───┘      └──┘
st            └──────────────────────────────────┘
191    by rw [prod_mul_distrib, this]; simp
id            └──────────────┘  └──┘
src       └──┘└──────────────┘└┘      └───┘
typ       └──┘└──────────────┘└┘└──┘  └───┘
doc       └──┘                └┘      └───┘
txt       └──┘                └┘      └───┘
par       └──┘                └┘      └───┘
pid         └┘                └┘          
st       └───────────────────┘└────┘└─────┘
192  ... = (-1)^((Ico 1 (p / 2).succ).filter
id              └─┘        └──┘  └────┘
src             └─┘         └──┘  └────┘
typ             └─┘        └──┘  └────┘
doc               └─┘                └────┘
193        (λ x : ℕ, ¬(a * x : zmodp p hp).val ≤ p / 2)).card * (p / 2).fact :
id                        └───┘  └┘ └─┘        └──┘        └──┘
src                         └───┘      └─┘         └──┘         └──┘
typ                       └───┘  └┘ └─┘        └──┘        └──┘
doc                                                     └──┘           └──┘
194    by rw [← prod_nat_cast, finset.prod_eq_multiset_prod,
id              └───────────┘  └──────────────────────────┘
src       └────┘└───────────┘└┘└──────────────────────────┘└─
typ       └────┘└───────────┘└┘└──────────────────────────┘└─
doc       └────┘             └┘                            └─
txt       └────┘             └┘                            └─
par       └────┘             └┘                            └─
pid         └──┘             └┘                            └─
st       └──────────────────┘└────────────────────────────┘└─
195        Ico_map_val_min_abs_nat_abs_eq_Ico_map_id hp a hpa,
id         └───────────────────────────────────────┘ └┘  └─┘
src  ─────┘└───────────────────────────────────────┘      └─
typ  ─────┘└───────────────────────────────────────┘└┘└─┘└─
doc  ─────┘└───────────────────────────────────────┘      └─
txt  ─────┘                                               └─
par  ─────┘                                               └─
pid  ─────┘                                               └─
st   ───────────────────────────────────────────────────────┘└─
196        ← finset.prod_eq_multiset_prod, prod_Ico_id_eq_fact]
id           └──────────────────────────┘  └─────────────────┘
src  ───────┘└──────────────────────────┘└┘└─────────────────┘└─
typ  ───────┘└──────────────────────────┘└┘└─────────────────┘└─
doc  ───────┘                            └┘                   └─
txt  ───────┘                            └┘                   └─
par  ───────┘                            └┘                   └─
pid  ───────┘                            └┘                   
st   ───────────────────────────────────┘└───────────────────┘
197  
src  
typ  
doc  
txt  
par  
pid  
st   
198  private lemma gauss_lemma_aux₂ {p : ℕ} (hp : p.prime) (hp2 : p % 2 = 1) {a : ℕ}
id                                               └────┘                      
src                                               └────┘                       
typ                                              └────┘                      
doc                                                └────┘
199    (hpa : (a : zmodp p hp) ≠ 0) :
id                └───┘  └┘  
src                └───┘       
typ               └───┘  └┘  
200    (a^(p / 2) : zmodp p hp) = (-1)^((Ico 1 (p / 2).succ).filter
id              └───┘  └┘        └─┘        └──┘  └────┘
src               └───┘             └─┘         └──┘  └────┘
typ             └───┘  └┘        └─┘        └──┘  └────┘
doc                                      └─┘                └────┘
201      (λ x : ℕ, p / 2 < (a * x : zmodp p hp).val)).card :=
id                           └───┘  └┘ └─┘   └──┘
src                             └───┘      └─┘   └──┘
typ                          └───┘  └┘ └─┘   └──┘
doc                                                  └──┘
202  (domain.mul_right_inj
id    └──────────────────┘
src   └──────────────────┘
typ   └──────────────────┘
doc   └──────────────────┘
203      (show ((p / 2).fact : zmodp p hp) ≠ 0,
id                   └──┘    └───┘  └┘  
src                   └──┘    └───┘       
typ                  └──┘    └───┘  └┘  
doc                    └──┘
204        by rw [ne.def, zmodp.eq_zero_iff_dvd_nat, hp.dvd_fact, not_le];
id                └────┘  └───────────────────────┘               └────┘
src           └──┘└────┘└┘└───────────────────────┘└┘           └┘└────┘
typ           └──┘└────┘└┘└───────────────────────┘└┘└─────────┘└┘└────┘
doc           └──┘      └┘                         └┘           └┘      
txt           └──┘      └┘                         └┘           └┘      
par           └──┘      └┘                         └┘           └┘      
pid             └┘      └┘                         └┘           └┘      
st           └─────────┘└─────────────────────────┘└───────────┘└──────┘└─
205            exact nat.div_lt_self hp.pos dec_trivial)).1 $
id                   └─────────────┘ └────┘ └─────────┘  
src            └────┘└─────────────┘└────┘└─────────┘  
typ            └────┘└─────────────┘└────┘└─────────┘  
doc            └────┘                     └─────────┘
txt            └────┘                     
par            └────┘                     
pid                                      
st   ─────────────────────────────────────────────────┘
206    by simpa using gauss_lemma_aux₁ _ hp2 hpa
id                    └──────────────┘   └─┘ └─┘
src       └──────────┘└──────────────┘└─┘      
typ       └──────────┘└──────────────┘└─┘└─┘└─┘
doc       └──────────┘                └─┘      
txt       └──────────┘                └─┘      
par       └──────────┘                └─┘      
pid            └────┘                └─┘      
st       └───────────────────────────────────────
207  
src  
typ  
doc  
txt  
par  
pid  
st   
208  private lemma eisenstein_lemma_aux₁ {p : ℕ} (hp : p.prime) (hp2 : p % 2 = 1) {a : ℕ}
id                                                    └────┘                      
src                                                    └────┘                       
typ                                                   └────┘                      
doc                                                     └────┘
209    (hap : (a : zmodp p hp) ≠ 0) :
id                └───┘  └┘  
src                └───┘       
typ               └───┘  └┘  
210    (((Ico 1 (p / 2).succ).sum (λ x, a * x) : ℕ) : zmod 2) =
id        └─┘        └──┘  └─┘                 └──┘    
src       └─┘         └──┘  └─┘                    └──┘    
typ       └─┘        └──┘  └─┘                 └──┘    
doc       └─┘
211      ((Ico 1 (p / 2).succ).filter
id         └─┘        └──┘  └────┘
src        └─┘         └──┘  └────┘
typ        └─┘        └──┘  └────┘
doc        └─┘                └────┘
212        ((λ x : ℕ, p / 2 < (a * x : zmodp p hp).val))).card +
id                              └───┘  └┘ └─┘    └──┘  
src                                └───┘      └─┘    └──┘  
typ                             └───┘  └┘ └─┘    └──┘  
doc                                                      └──┘
213        (Ico 1 (p / 2).succ).sum (λ x, x)
id          └─┘        └──┘  └─┘       
src         └─┘         └──┘  └─┘
typ         └─┘        └──┘  └─┘       
doc         └─┘
214      + ((Ico 1 (p / 2).succ).sum (λ x, (a * x) / p) : ℕ) :=
id          └─┘        └──┘  └─┘                 
src         └─┘         └──┘  └─┘                     
typ         └─┘        └──┘  └─┘                 
doc          └─┘
215  have hp2 : (p : zmod 2) = (1 : ℕ), from zmod.eq_iff_modeq_nat.2 hp2,
id                  └──┘                  └───────────────────┘  └─┘
src                  └──┘                  └───────────────────┘
typ                 └──┘                  └───────────────────┘  └─┘
216  calc (((Ico 1 (p / 2).succ).sum (λ x, a * x) : ℕ) : zmod 2)
id           └─┘        └──┘  └─┘                 └──┘
src          └─┘         └──┘  └─┘                    └──┘
typ          └─┘        └──┘  └─┘                 └──┘
doc          └─┘
217      = (((Ico 1 (p / 2).succ).sum (λ x, (a * x) % p + p * ((a * x) / p)) : ℕ) : zmod 2) :
id            └─┘        └──┘  └─┘                                 └──┘
src           └─┘         └──┘  └─┘                                         └──┘
typ           └─┘        └──┘  └─┘                                 └──┘
doc           └─┘
218    by simp only [mod_add_div]
id                   └─────────┘
src       └─────────┘└─────────┘└┘
typ       └─────────┘└─────────┘└┘
doc       └─────────┘           └┘
txt       └─────────┘           └┘
par       └─────────┘           └┘
pid           └──┘└┘           
st       └───────────────────────┘
219  ... = ((Ico 1 (p / 2).succ).sum (λ x, ((a * x : ℕ) : zmodp p hp).val) : ℕ) +
id           └─┘        └──┘  └─┘                  └───┘  └┘ └─┘       
src          └─┘         └──┘  └─┘                     └───┘      └─┘       
typ          └─┘        └──┘  └─┘                  └───┘  └┘ └─┘       
doc          └─┘
220      ((Ico 1 (p / 2).succ).sum (λ x, (a * x) / p) : ℕ) :
id         └─┘        └──┘  └─┘                 
src        └─┘         └──┘  └─┘                     
typ        └─┘        └──┘  └─┘                 
doc        └─┘
221    by simp only [zmodp.val_cast_nat];
id                   └────────────────┘
src       └─────────┘└────────────────┘
typ       └─────────┘└────────────────┘
doc       └─────────┘                  
txt       └─────────┘                  
par       └─────────┘                  
pid           └──┘└┘                  
st       └────────────────────────────────
222      simp [sum_add_distrib, mul_sum.symm, nat.cast_add, nat.cast_mul, sum_nat_cast, hp2]
id             └─────────────┘                └──────────┘  └──────────┘  └──────────┘  └─┘
src      └────┘└─────────────┘└┘            └┘└──────────┘└┘└──────────┘└┘└──────────┘└┘   └┘
typ      └────┘└─────────────┘└┘└──────────┘└┘└──────────┘└┘└──────────┘└┘└──────────┘└┘└─┘└┘
doc      └────┘               └┘            └┘            └┘            └┘            └┘   └┘
txt      └────┘               └┘            └┘            └┘            └┘            └┘   └┘
par      └────┘               └┘            └┘            └┘            └┘            └┘   └┘
pid                         └┘            └┘            └┘            └┘            └┘   
st   ───────────────────────────────────────────────────────────────────────────────────────┘
223  ... = _ : congr_arg2 (+)
id             └────────┘ 
src            └────────┘ 
typ            └────────┘ 
224    (calc (((Ico 1 (p / 2).succ).sum (λ x, ((a * x : ℕ) : zmodp p hp).val) : ℕ) : zmod 2)
id              └─┘        └──┘  └─┘                  └───┘  └┘ └─┘         └──┘
src             └─┘         └──┘  └─┘                     └───┘      └─┘         └──┘
typ             └─┘        └──┘  └─┘                  └───┘  └┘ └─┘         └──┘
doc             └─┘
225        = (Ico 1 (p / 2).succ).sum
id            └─┘        └──┘  └─┘
src           └─┘         └──┘  └─┘
typ           └─┘        └──┘  └─┘
doc           └─┘
226            (λ x, ((((a * x : zmodp p hp).val_min_abs +
id                           └───┘  └┘ └─────────┘  
src                             └───┘      └─────────┘  
typ                          └───┘  └┘ └─────────┘  
doc                                         └─────────┘
227              (if (a * x : zmodp p hp).val ≤ p / 2 then 0 else p)) : ℤ) : zmod 2)) :
id                         └───┘  └┘ └─┘                            └──┘
src                          └───┘      └─┘                              └──┘
typ                        └───┘  └┘ └─┘                            └──┘
228          by simp only [(zmodp.val_eq_ite_val_min_abs _).symm]; simp [sum_nat_cast]
id                          └──────────────────────────┘                 └──────────┘
src             └─────────┘ └──────────────────────────┘└───────┘  └────┘└──────────┘└─
typ             └─────────┘ └──────────────────────────┘└───────┘  └────┘└──────────┘└─
doc             └─────────┘                             └───────┘  └────┘            └─
txt             └─────────┘                             └───────┘  └────┘            └─
par             └─────────┘                             └───────┘  └────┘            └─
pid                 └──┘└┘                             └───────┘                  
st             └───────────────────────────────────────────────────────────────────────
229    ... = ((Ico 1 (p / 2).succ).filter
id             └─┘        └──┘  └────┘
src  ─┘        └─┘         └──┘  └────┘
typ  ─┘        └─┘        └──┘  └────┘
doc  ─┘        └─┘                └────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
230          (λ x : ℕ, p / 2 < (a * x : zmodp p hp).val)).card +
id                               └───┘  └┘ └─┘   └──┘  
src                                 └───┘      └─┘   └──┘  
typ                              └───┘  └┘ └─┘   └──┘  
doc                                                      └──┘
231        (((Ico 1 (p / 2).succ).sum (λ x, (a * x : zmodp p hp).val_min_abs.nat_abs)) : ℕ) :
id            └─┘        └──┘  └─┘             └───┘  └┘ └─────────┘ └─────┘      
src           └─┘         └──┘  └─┘                └───┘      └─────────┘ └─────┘      
typ           └─┘        └──┘  └─┘             └───┘  └┘ └─────────┘ └─────┘      
doc           └─┘                                               └─────────┘
232      by simp [sum_add_distrib, finset.sum_ite, hp2, sum_nat_cast]
id                └─────────────┘  └────────────┘  └─┘  └──────────┘
src         └────┘└─────────────┘└┘└────────────┘└┘   └┘└──────────┘└─
typ         └────┘└─────────────┘└┘└────────────┘└┘└─┘└┘└──────────┘└─
doc         └────┘               └┘              └┘   └┘            └─
txt         └────┘               └┘              └┘   └┘            └─
par         └────┘               └┘              └┘   └┘            └─
pid                            └┘              └┘   └┘            
st         └──────────────────────────────────────────────────────────
233    ... = _ : by rw [finset.sum_eq_multiset_sum,
id                      └────────────────────────┘
src  ─┘             └──┘└────────────────────────┘└─
typ  ─┘             └──┘└────────────────────────┘└─
doc  ─┘             └──┘                          └─
txt  ─┘             └──┘                          └─
par  ─┘             └──┘                          └─
pid  ─┘               └┘                          └─
st   ─┘            └─────────────────────────────┘└─
234        Ico_map_val_min_abs_nat_abs_eq_Ico_map_id hp _ hap,
id         └───────────────────────────────────────┘ └┘   └─┘
src  ─────┘└───────────────────────────────────────┘  └─┘   └─
typ  ─────┘└───────────────────────────────────────┘└┘└─┘└─┘└─
doc  ─────┘└───────────────────────────────────────┘  └─┘   └─
txt  ─────┘                                           └─┘   └─
par  ─────┘                                           └─┘   └─
pid  ─────┘                                           └─┘   └─
st   ───────────────────────────────────────────────────────┘└─
235        ← finset.sum_eq_multiset_sum];
id           └────────────────────────┘
src  ───────┘└────────────────────────┘
typ  ───────┘└────────────────────────┘
doc  ───────┘                          
txt  ───────┘                          
par  ───────┘                          
pid  ───────┘                          
st   ─────────────────────────────────┘└─
236      simp [sum_nat_cast]) rfl
id             └──────────┘   └─┘
src      └────┘└──────────┘  └─┘
typ      └────┘└──────────┘  └─┘
doc      └────┘            
txt      └────┘            
par      └────┘            
pid                      
st   ──────────────────────┘
237  
238  private lemma eisenstein_lemma_aux₂ {p : ℕ} (hp : p.prime) (hp2 : p % 2 = 1) {a : ℕ} (ha2 : a % 2 = 1)
id                                                    └────┘                                   
src                                                    └────┘                                     
typ                                                   └────┘                                   
doc                                                     └────┘
239    (hap : (a : zmodp p hp) ≠ 0) :
id                └───┘  └┘  
src                └───┘       
typ               └───┘  └┘  
240    ((Ico 1 (p / 2).succ).filter
id       └─┘        └──┘  └────┘
src      └─┘         └──┘  └────┘
typ      └─┘        └──┘  └────┘
doc      └─┘                └────┘
241      ((λ x : ℕ, p / 2 < (a * x : zmodp p hp).val))).card
id                            └───┘  └┘ └─┘    └──┘
src                              └───┘      └─┘    └──┘
typ                           └───┘  └┘ └─┘    └──┘
doc                                                    └──┘
242    ≡ (Ico 1 (p / 2).succ).sum (λ x, (x * a) / p) [MOD 2] :=
id       └─┘        └──┘  └─┘               └──┘  
src      └─┘         └──┘  └─┘                   └──┘  
typ      └─┘        └──┘  └─┘               └──┘  
doc      └─┘                                        └──┘  
243  have ha2 : (a : zmod 2) = (1 : ℕ), from zmod.eq_iff_modeq_nat.2 ha2,
id                  └──┘                  └───────────────────┘  └─┘
src                  └──┘                  └───────────────────┘
typ                 └──┘                  └───────────────────┘  └─┘
244  (@zmod.eq_iff_modeq_nat 2 _ _).1 $ sub_eq_zero.1 $
id     └───────────────────┘           └─────────┘
src    └───────────────────┘           └─────────┘
typ    └───────────────────┘           └─────────┘
245    by simpa [finset.mul_sum.symm, mul_comm, ha2, sum_nat_cast, add_neg_eq_iff_eq_add.symm,
id                                    └──────┘  └─┘  └──────────┘
src       └─────┘                   └┘└──────┘└┘   └┘└──────────┘└┘                          └─
typ       └─────┘└─────────────────┘└┘└──────┘└┘└─┘└┘└──────────┘└┘└────────────────────────┘└─
doc       └─────┘                   └┘        └┘   └┘            └┘                          └─
txt       └─────┘                   └┘        └┘   └┘            └┘                          └─
par       └─────┘                   └┘        └┘   └┘            └┘                          └─
pid                               └┘        └┘   └┘            └┘                          └─
st       └─────────────────────────────────────────────────────────────────────────────────────
246      zmod.neg_eq_self_mod_two] using eq.symm (eisenstein_lemma_aux₁ hp hp2 hap)
id       └──────────────────────┘        └─────┘  └───────────────────┘ └┘ └─┘ └─┘
src  ───┘└──────────────────────┘└──────┘└─────┘ └───────────────────┘        └─
typ  ───┘└──────────────────────┘└──────┘└─────┘ └───────────────────┘└┘└─┘└─┘└─
doc  ───┘                        └──────┘                                     └─
txt  ───┘                        └──────┘                                     └─
par  ───┘                        └──────┘                                     └─
pid  ───┘                        └────┘                                     
st   ───────────────────────────────────────────────────────────────────────────────
247  
src  
typ  
doc  
txt  
par  
pid  
st   
248  lemma div_eq_filter_card {a b c : ℕ} (hb0 : 0 < b) (hc : a / b ≤ c) : a / b =
id                                                                    
src                                                                         
typ                                                                   
249    ((Ico 1 c.succ).filter (λ x, x * b ≤ a)).card :=
id       └─┘   └───┘ └────┘             └──┘
src      └─┘    └───┘ └────┘                 └──┘
typ      └─┘   └───┘ └────┘             └──┘
doc      └─┘          └────┘                   └──┘
250  calc a / b = (Ico 1 (a / b).succ).card : by simp
id              └─┘       └──┘  └──┘
src               └─┘         └──┘  └──┘       └───┘
typ             └─┘       └──┘  └──┘       └───┘
doc                └─┘                └──┘       └───┘
txt                                              └───┘
par                                              └───┘
pid                                                  
st                                              └────┘
251  ... = ((Ico 1 c.succ).filter (λ x, x * b ≤ a)).card :
id           └─┘   └───┘ └────┘             └──┘
src          └─┘    └───┘ └────┘                 └──┘
typ          └─┘   └───┘ └────┘             └──┘
doc          └─┘          └────┘                   └──┘
252    congr_arg _$ finset.ext.2 $ λ x,
id     └───────┘    └────────┘      
src    └───────┘    └────────┘
typ    └───────┘    └────────┘      
253      have x * b ≤ a → x ≤ c,
id                     
src                       
typ                    
254        from λ h, le_trans (by rwa [le_div_iff_mul_le _ _ hb0]) hc,
id                  └──────┘          └───────────────┘     └─┘   └┘
src                  └──────┘     └───┘└───────────────┘└───┘   
typ                 └──────┘     └───┘└───────────────┘└───┘└─┘  └┘
doc                               └───┘                 └───┘   
txt                               └───┘                 └───┘   
par                               └───┘                 └───┘   
pid                                  └┘                 └───┘   
st                               └─────────────────────────────┘
255      by simp [lt_succ_iff, le_div_iff_mul_le _ _ hb0]; tauto
id                └─────────┘  └───────────────┘     └─┘
src         └────┘└─────────┘└┘└───────────────┘└───┘     └─────
typ         └────┘└─────────┘└┘└───────────────┘└───┘└─┘  └─────
doc         └────┘           └┘                 └───┘     └─────
txt         └────┘           └┘                 └───┘     └─────
par         └────┘           └┘                 └───┘     └─────
pid                        └┘                 └───┘          
st         └─────────────────────────────────────────────────────
256  
src  
typ  
doc  
txt  
par  
pid  
st   
257  /-- The given sum is the number of integers point in the triangle formed by the diagonal of the
258    rectangle `(0, p/2) × (0, q/2)`  -/
259  private lemma sum_Ico_eq_card_lt {p q : ℕ} :
id                                           
src                                          
typ                                          
260    (Ico 1 (p / 2).succ).sum (λ a, (a * q) / p) =
id      └─┘        └──┘  └─┘               
src     └─┘         └──┘  └─┘                   
typ     └─┘        └──┘  └─┘               
doc     └─┘
261    (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id        └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
src       └─┘         └──┘  └─────┘   └─┘         └──┘   └────┘
typ       └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
doc       └─┘                └─────┘   └─┘                 └────┘
262    (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q)).card :=
id                          └──┘
src                             └──┘
typ                         └──┘
doc                                     └──┘
263  if hp0 : p = 0 then by simp [hp0, finset.ext]
id   └┘                         └─┘  └────────┘
src  └┘                    └────┘   └┘└────────┘└┘
typ  └┘                   └────┘└─┘└┘└────────┘└┘
doc                         └────┘   └┘          └┘
txt                         └────┘   └┘          └┘
par                         └────┘   └┘          └┘
pid                                └┘          
st                         └──────────────────────┘
264  else
265    calc (Ico 1 (p / 2).succ).sum (λ a, (a * q) / p) =
id           └─┘        └──┘  └─┘             
src          └─┘         └──┘  └─┘               
typ          └─┘        └──┘  └─┘             
doc          └─┘
266      (Ico 1 (p / 2).succ).sum (λ a,
id        └─┘        └──┘  └─┘     
src       └─┘         └──┘  └─┘
typ       └─┘        └──┘  └─┘     
doc       └─┘
267        ((Ico 1 (q / 2).succ).filter (λ x, x * p ≤ a * q)).card) :
id           └─┘        └──┘  └────┘               └──┘
src          └─┘         └──┘  └────┘                    └──┘
typ          └─┘        └──┘  └────┘               └──┘
doc          └─┘                └────┘                       └──┘
268      finset.sum_congr rfl $ λ x hx,
id       └──────────────┘ └─┘      └┘
src      └──────────────┘ └─┘
typ      └──────────────┘ └─┘      └┘
269        div_eq_filter_card (nat.pos_of_ne_zero hp0)
id         └────────────────┘  └────────────────┘ └─┘
src        └────────────────┘  └────────────────┘
typ        └────────────────┘  └────────────────┘ └─┘
270          (calc x * q / p ≤ (p / 2) * q / p :
id                                 
src                                    
typ                                
271              nat.div_le_div_right (mul_le_mul_of_nonneg_right
id               └──────────────────┘  └────────────────────────┘
src              └──────────────────┘  └────────────────────────┘
typ              └──────────────────┘  └────────────────────────┘
272                (le_of_lt_succ $ by finish)
id                  └───────────┘
src                 └───────────┘      └────┘
typ                 └───────────┘      └────┘
doc                                    └────┘
txt                                    └────┘
par                                    └────┘
st                                    └─────┘
273                (nat.zero_le _))
id                  └─────────┘
src                 └─────────┘
typ                 └─────────┘
274            ... ≤ _ : nat.div_mul_div_le_div _ _ _)
id                       └────────────────────┘
src                      └────────────────────┘
typ                      └────────────────────┘
275    ... = _ : by rw [← card_sigma];
id     └─┘                └────────┘
src    └─┘          └────┘└────────┘
typ    └─┘          └────┘└────────┘
doc                 └────┘          
txt                 └────┘          
par                 └────┘          
pid                   └──┘          
st                 └───────────────┘└─
276      exact card_congr (λ a _, ⟨a.1, a.2⟩)
id             └────────┘
src      └────┘└────────┘  └────┘  └──┘ └────
typ      └────┘└────────┘  └────┘  └──┘ └────
doc      └────┘            └────┘  └──┘ └────
txt      └────┘            └────┘  └──┘ └────
par      └────┘            └────┘  └──┘ └────
pid                       └────┘  └──┘ └────
st   ─────────────────────────────────────────
277        (by simp {contextual := tt})
id                                 └┘
src  ─────┘   └───┘ └────────────┘└┘└─
typ  ─────┘   └───┘ └────────────┘└┘└─
doc  ─────┘   └───┘ └────────────┘  └─
txt  ─────┘   └───┘ └────────────┘  └─
par  ─────┘   └───┘ └────────────┘  └─
pid  ─────┘   └────┘ └────────────┘  └──
st   ────────┘└──────────────────────┘└─
278        (λ ⟨_, _⟩ ⟨_, _⟩, by simp {contextual := tt})
id                                                  └┘
src  ─────┘  └──────────────┘  └───┘ └────────────┘└┘└─
typ  ─────┘  └──────────────┘  └───┘ └────────────┘└┘└─
doc  ─────┘  └──────────────┘  └───┘ └────────────┘  └─
txt  ─────┘  └──────────────┘  └───┘ └────────────┘  └─
par  ─────┘  └──────────────┘  └───┘ └────────────┘  └─
pid  ─────┘  └──────────────┘  └────┘ └────────────┘  └──
st   ─────────────────────────┘└──────────────────────┘└─
279        (λ ⟨b₁, b₂⟩ h, ⟨⟨b₁, b₂⟩,
id             └┘  └┘
src  ─────┘  └┘  └┘  └───┘    └┘  └──
typ  ─────┘  └┘└┘└┘└┘└───┘    └┘  └──
doc  ─────┘  └┘  └┘  └───┘    └┘  └──
txt  ─────┘  └┘  └┘  └───┘    └┘  └──
par  ─────┘  └┘  └┘  └───┘    └┘  └──
pid  ─────┘  └┘  └┘  └───┘    └┘  └──
st   ────────────────────────────────
280          by revert h; simp {contextual := tt}⟩)
id                                            └┘
src  ───────┘  └──────┘└┘└───┘ └────────────┘└┘└──
typ  ───────┘  └──────┘└┘└───┘ └────────────┘└┘└──
doc  ───────┘  └──────┘└┘└───┘ └────────────┘  └──
txt  ───────┘  └──────┘└┘└───┘ └────────────┘  └──
par  ───────┘  └──────┘└┘└───┘ └────────────┘  └──
pid  ───────┘  └──────────────┘ └────────────┘  └─┘
st   ─────────┘└────────────────────────────────┘└──
281  
src  
typ  
doc  
txt  
par  
pid  
st   
282  /-- Each of the sums in this lemma is the cardinality of the set integer points in each of the
283    two triangles formed by the diagonal of the rectangle `(0, p/2) × (0, q/2)`. Adding them
284    gives the number of points in the rectangle. -/
285  private lemma sum_mul_div_add_sum_mul_div_eq_mul {p q : ℕ} (hp : p.prime)
id                                                                   └────┘
src                                                                   └────┘
typ                                                                  └────┘
doc                                                                    └────┘
286    (hq0 : (q : zmodp p hp) ≠ 0) :
id                └───┘  └┘  
src                └───┘       
typ               └───┘  └┘  
287    (Ico 1 (p / 2).succ).sum (λ a, (a * q) / p) +
id      └─┘        └──┘  └─┘               
src     └─┘         └──┘  └─┘                   
typ     └─┘        └──┘  └─┘               
doc     └─┘
288    (Ico 1 (q / 2).succ).sum (λ a, (a * p) / q) =
id      └─┘        └──┘  └─┘               
src     └─┘         └──┘  └─┘                   
typ     └─┘        └──┘  └─┘               
doc     └─┘
289    (p / 2) * (q / 2) :=
id              
src               
typ             
290  have hswap : (((Ico 1 (q / 2).succ).product (Ico 1 (p / 2).succ)).filter
id                   └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
src                  └─┘         └──┘  └─────┘   └─┘         └──┘   └────┘
typ                  └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
doc                  └─┘                └─────┘   └─┘                 └────┘
291      (λ x : ℕ × ℕ, x.2 * q ≤ x.1 * p)).card =
id                            └──┘  
src                               └──┘  
typ                           └──┘  
doc                                       └──┘
292    (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id        └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
src       └─┘         └──┘  └─────┘   └─┘         └──┘   └────┘
typ       └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
doc       └─┘                └─────┘   └─┘                 └────┘
293      (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p)).card :=
id                            └──┘
src                               └──┘
typ                           └──┘
doc                                       └──┘
294    card_congr (λ x _, prod.swap x)
id     └────────┘       └───────┘ 
src    └────────┘         └───────┘
typ    └────────┘       └───────┘ 
doc                       └───────┘
295      (λ ⟨_, _⟩, by simp {contextual := tt})
id                                        └┘
src                    └───┘ └────────────┘└┘
typ                   └───┘ └────────────┘└┘
doc                    └───┘ └────────────┘  
txt                    └───┘ └────────────┘  
par                    └───┘ └────────────┘  
pid                         └────────────┘  
st                    └──────────────────────┘
296      (λ ⟨_, _⟩ ⟨_, _⟩, by simp {contextual := tt})
id                                              └┘
src                           └───┘ └────────────┘└┘
typ                         └───┘ └────────────┘└┘
doc                           └───┘ └────────────┘  
txt                           └───┘ └────────────┘  
par                           └───┘ └────────────┘  
pid                                └────────────┘  
st                           └──────────────────────┘
297      (λ ⟨x₁, x₂⟩ h, ⟨⟨x₂, x₁⟩, by revert h; simp {contextual := tt}⟩),
id          └┘  └┘                                                └┘
src                                   └──────┘  └───┘ └────────────┘└┘
typ         └┘  └┘                  └──────┘  └───┘ └────────────┘└┘
doc                                   └──────┘  └───┘ └────────────┘  
txt                                   └──────┘  └───┘ └────────────┘  
par                                   └──────┘  └───┘ └────────────┘  
pid                                         └┘       └────────────┘  
st                                   └────────────────────────────────┘
298  have hdisj : disjoint
id                └──────┘
src               └──────┘
typ               └──────┘
doc               └──────┘
299      (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id          └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
src         └─┘         └──┘  └─────┘   └─┘         └──┘   └────┘
typ         └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
doc         └─┘                └─────┘   └─┘                 └────┘
300        (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q))
id                            
src                             
typ                           
301      (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id          └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
src         └─┘         └──┘  └─────┘   └─┘         └──┘   └────┘
typ         └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
doc         └─┘                └─────┘   └─┘                 └────┘
302        (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p)),
id                            
src                             
typ                           
303    from disjoint_filter.2 $ λ x hx hpq hqp,
id          └─────────────┘       └┘ └─┘ └─┘
src         └─────────────┘
typ         └─────────────┘       └┘ └─┘ └─┘
304    have hxp : x.1 < p, from lt_of_le_of_lt
id                          └────────────┘
src                           └────────────┘
typ                         └────────────┘
305      (show x.1 ≤ p / 2, by simp [*, nat.lt_succ_iff] at *; tauto)
id                                 └─────────────┘
src                         └───────┘└─────────────┘└────┘  └───┘
typ                       └───────┘└─────────────┘└────┘  └───┘
doc                            └───────┘               └────┘  └───┘
txt                            └───────┘               └────┘  └───┘
par                            └───────┘               └────┘  └───┘
pid                                └──┘               └──┘
st                            └────────────────────────────────────┘
306      (nat.div_lt_self hp.pos dec_trivial),
id        └─────────────┘ └┘└──┘ └─────────┘
src       └─────────────┘   └──┘ └─────────┘
typ       └─────────────┘ └┘└──┘ └─────────┘
doc                              └─────────┘
307    begin
st     └─────
308      have : (x.1 : zmodp p hp) = 0,
id                    └───┘  └┘  
src      └─────┘  └───┘└───┘   └┘└┘
typ      └─────┘ └───┘└───┘└┘└┘└┘
doc      └─────┘  └───┘        └┘ └┘
txt      └─────┘  └───┘        └┘ └┘
par      └─────┘  └───┘        └┘ └┘
pid      └───┘└┘  └───┘        └┘ 
st   ────────────────────────────────┘└─
309      { simpa [hq0] using congr_arg (coe : ℕ → zmodp p hp) (le_antisymm hpq hqp) },
id                └─┘        └───────┘  └─┘       └───┘  └┘   └─────────┘ └─┘ └─┘
src        └─────┘   └──────┘└───────┘ └─┘└─┘  └───┘   └┘ └─────────┘      └┘
typ        └─────┘└─┘└──────┘└───────┘ └─┘└─┘  └───┘└┘└┘ └─────────┘└─┘└─┘└┘
doc        └─────┘   └──────┘             └─┘          └┘                  └┘
txt        └─────┘   └──────┘             └─┘          └┘                  └┘
par        └─────┘   └──────┘             └─┘          └┘                  └┘
pid                └────┘             └─┘          └┘                  
st   ─────┘└───────────────────────────────────────────────────────────────────────┘└┘
310      rw [fin.eq_iff_veq, zmodp.val_cast_of_lt hp hxp, zmodp.zero_val] at this,
id           └────────────┘  └──────────────────┘ └┘ └─┘  └────────────┘
src      └──┘└────────────┘└┘└──────────────────┘     └┘└────────────┘└───────┘
typ      └──┘└────────────┘└┘└──────────────────┘└┘└─┘└┘└────────────┘└───────┘
doc      └──┘              └┘                         └┘              └───────┘
txt      └──┘              └┘                         └┘              └───────┘
par      └──┘              └┘                         └┘              └───────┘
pid        └┘              └┘                         └┘              └──────┘
st   ─────────────────────┘└───────────────────────────┘└──────────────┘└──────┘└─
311      simp * at *
src      └───────────
typ      └───────────
doc      └───────────
txt      └───────────
par      └───────────
pid          └──┘
st   ────────────────
312    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
313  have hunion : ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id                   └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
src                  └─┘         └──┘  └─────┘   └─┘         └──┘   └────┘
typ                  └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
doc                  └─┘                └─────┘   └─┘                 └────┘
314        (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q) ∪
id                              
src                                 
typ                             
315      ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id         └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
src        └─┘         └──┘  └─────┘   └─┘         └──┘   └────┘
typ        └─┘        └──┘  └─────┘   └─┘        └──┘   └────┘
doc        └─┘                └─────┘   └─┘                 └────┘
316        (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p) =
id                              
src                                 
typ                             
317      ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)),
id         └─┘        └──┘  └─────┘   └─┘        └──┘
src        └─┘         └──┘  └─────┘   └─┘         └──┘
typ        └─┘        └──┘  └─────┘   └─┘        └──┘
doc        └─┘                └─────┘   └─┘
318    from finset.ext.2 $ λ x, by have := le_total (x.2 * p) (x.1 * q); simp; tauto,
id          └────────┘                   └──────┘               
src         └────────┘            └──────┘└──────┘  └─┘ └┘  └─┘    └──┘  └───┘
typ         └────────┘           └──────┘└──────┘  └─┘└┘ └─┘   └──┘  └───┘
doc                                └──────┘          └─┘  └┘  └─┘    └──┘  └───┘
txt                                └──────┘          └─┘  └┘  └─┘    └──┘  └───┘
par                                └──────┘          └─┘  └┘  └─┘    └──┘  └───┘
pid                                └───┘└─┘          └─┘  └┘  └─┘  
st                                └────────────────────────────────────────────────┘
319  by rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_disjoint_union hdisj, hunion,
id          └────────────────┘  └────────────────┘  └───┘    └─────────────────┘ └───┘  └────┘
src     └──┘└────────────────┘└┘└────────────────┘└┘     └──┘└─────────────────┘     └┘      └─
typ     └──┘└────────────────┘└┘└────────────────┘└┘└───┘└──┘└─────────────────┘└───┘└┘└────┘└─
doc     └──┘└────────────────┘└┘└────────────────┘└┘     └──┘                        └┘      └─
txt     └──┘                  └┘                  └┘     └──┘                        └┘      └─
par     └──┘                  └┘                  └┘     └──┘                        └┘      └─
pid       └┘                  └┘                  └┘     └──┘                        └┘      └─
st     └─────────────────────┘└──────────────────┘└─────┘└───────────────────────────┘└──────┘└─
320      card_product];
id       └──────────┘
src  ───┘└──────────┘
typ  ───┘└──────────┘
doc  ───┘            
txt  ───┘            
par  ───┘            
pid  ───┘            
st   ───────────────┘└─
321    simp
src    └────
typ    └────
doc    └────
txt    └────
par    └────
pid        
st   ───────
322  
src  
typ  
doc  
txt  
par  
pid  
st   
323  variables {p q : ℕ} (hp : nat.prime p) (hq : nat.prime q)
id                           └───────┘          └───────┘
src                           └───────┘          └───────┘
typ                          └───────┘          └───────┘
doc                            └───────┘          └───────┘
324  
325  namespace zmodp
326  
327  def legendre_sym (a p : ℕ) (hp : nat.prime p) : ℤ :=
id                                   └───────┘     
src                                  └───────┘      
typ                                  └───────┘     
doc                                   └───────┘
328  if (a : zmodp p hp) = 0 then 0 else if ∃ b : zmodp p hp, b ^ 2 = a then 1 else -1
id          └───┘  └┘                         └───┘  └┘                   
src          └───┘                              └───┘                          
typ         └───┘  └┘                         └───┘  └┘                   
329  
330  lemma legendre_sym_eq_pow (a p : ℕ) (hp : nat.prime p) :
id                                            └───────┘ 
src                                           └───────┘
typ                                           └───────┘ 
doc                                            └───────┘
331    (legendre_sym a p hp : zmodp p hp) = (a ^ (p / 2)) :=
id      └──────────┘   └┘   └───┘  └┘        
src     └──────────┘          └───┘               
typ     └──────────┘   └┘   └───┘  └┘        
332  if ha : (a : zmodp p hp) = 0 then by simp [*, legendre_sym, _root_.zero_pow (nat.div_pos hp.two_le (succ_pos 1))]
id   └┘          └───┘  └┘                      └──────────┘  └─────────────┘  └─────────┘ └───────┘  └──────┘
src  └┘           └───┘                  └───────┘└──────────┘└┘└─────────────┘ └─────────┘└───────┘ └──────┘└────┘
typ  └┘          └───┘  └┘             └───────┘└──────────┘└┘└─────────────┘ └─────────┘└───────┘ └──────┘└────┘
doc                                       └───────┘            └┘                                             └────┘
txt                                       └───────┘            └┘                                             └────┘
par                                       └───────┘            └┘                                             └────┘
pid                                           └──┘            └┘                                             └───┘
st                                       └────────────────────────────────────────────────────────────────────────────┘
333  else
334  (nat.prime.eq_two_or_odd hp).elim
id    └─────────────────────┘ └┘ └──┘
src   └─────────────────────┘    └──┘
typ   └─────────────────────┘ └┘ └──┘
335    (λ hp2, begin resetI; subst hp2,
id        └─┘                      └─┘
src                  └────┘  └────┘
typ       └─┘        └────┘  └────┘└─┘
doc                  └────┘  └────┘
txt                  └────┘  └────┘
par                  └────┘  └────┘
pid                               
st             └─────────────────────┘└─
336      suffices : ∀ a : zmodp 2 nat.prime_two,
id                        └───┘
src      └─────────┘ └───┘     └─┘              
typ      └─────────┘ └───┘└───┘└─┘              
doc      └─────────┘ └───┘     └─┘              
txt      └─────────┘ └───┘     └─┘              
par      └─────────┘ └───┘     └─┘              
pid      └───────┘└┘ └───┘     └─┘              
st   ────────────────────────────────────────────
337        (((ite (a = 0) 0 (ite (∃ (b : zmodp 2 hp), b ^ 2 = a) 1 (-1))) : ℤ) : zmodp 2 nat.prime_two) = a ^ (2 / 2),
id                          └─┘        └───┘   └┘                                   └───────────┘           
src  ─────┘        └────┘ └─┘ └────┘└───┘└─┘   └─┘  └──┘ └─────┘ └──┘     └─┘└───────────┘└┘    └┘└─┘
typ  ─────┘        └────┘ └─┘ └────┘└───┘└─┘└┘ └─┘  └──┘ └─────┘ └──┘     └─┘└───────────┘└┘    └┘└─┘
doc  ─────┘         └────┘      └────┘     └─┘     └─┘  └──┘  └─────┘ └──┘     └─┘             └┘    └┘ └─┘
txt  ─────┘         └────┘      └────┘     └─┘     └─┘  └──┘  └─────┘ └──┘     └─┘             └┘    └┘ └─┘
par  ─────┘         └────┘      └────┘     └─┘     └─┘  └──┘  └─────┘ └──┘     └─┘             └┘    └┘ └─┘
pid  ─────┘         └────┘      └────┘     └─┘     └─┘  └──┘  └─────┘ └──┘     └─┘             └┘    └┘ └─┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
338      { exact this a },
id               └──┘ 
src        └────┘     
typ        └────┘└──┘
doc        └────┘     
txt        └────┘     
par        └────┘     
pid                  
st   ─────┘└───────────┘└┘
339      exact dec_trivial,
id             └─────────┘
src      └────┘└─────────┘
typ      └────┘└─────────┘
doc      └────┘└─────────┘
txt      └────┘
par      └────┘
pid           
st   ────────────────────┘└─
340     end)
st   ─────┘
341    (λ hp1, have _ := euler_criterion hp ha,
id        └─┘            └─────────────┘ └┘ └┘
src                      └─────────────┘
typ       └─┘            └─────────────┘ └┘ └┘
342      have (-1 : zmodp p hp) ≠ 1, from (ne_neg_self hp hp1 zero_ne_one.symm).symm,
id                 └───┘  └┘            └─────────┘ └┘ └─┘ └─────────┘└───┘ └──┘
src                └───┘                 └─────────┘        └─────────┘└───┘ └──┘
typ                └───┘  └┘            └─────────┘ └┘ └─┘ └─────────┘└───┘ └──┘
343      by cases zmodp.pow_div_two_eq_neg_one_or_one hp ha; simp [legendre_sym, *] at *)
id                └─────────────────────────────────┘ └┘ └┘        └──────────┘
src         └────┘└─────────────────────────────────┘      └────┘└──────────┘└───────┘
typ         └────┘└─────────────────────────────────┘└┘└┘  └────┘└──────────┘└───────┘
doc         └────┘                                         └────┘            └───────┘
txt         └────┘                                         └────┘            └───────┘
par         └────┘                                         └────┘            └───────┘
pid                                                                       └──┘└──┘
st         └───────────────────────────────────────────────────────────────────────────┘
344  
345  lemma legendre_sym_eq_one_or_neg_one (a : ℕ) (hp : nat.prime p) (ha : (a : zmodp p hp) ≠ 0) :
id                                                     └───────┘             └───┘  └┘  
src                                                    └───────┘               └───┘       
typ                                                    └───────┘             └───┘  └┘  
doc                                                     └───────┘
346    legendre_sym a p hp = -1 ∨ legendre_sym a p hp = 1 :=
id     └──────────┘   └┘     └──────────┘   └┘ 
src    └──────────┘            └──────────┘        
typ    └──────────┘   └┘     └──────────┘   └┘ 
347  by unfold legendre_sym; split_ifs; simp * at *
src     └─────────────────┘  └───────┘  └───────────
typ     └─────────────────┘  └───────┘  └───────────
doc     └─────────────────┘  └───────┘  └───────────
txt     └─────────────────┘  └───────┘  └───────────
par     └─────────────────┘  └───────┘  └───────────
pid           └───────────┘                 └──┘
st     └────────────────────────────────────────────
348  
src  
typ  
doc  
txt  
par  
pid  
st   
349  /-- Gauss' lemma. The legendre symbol can be computed by considering the number of naturals less
350    than `p/2` such that `(a * x) % p > p / 2` -/
351  lemma gauss_lemma {a : ℕ} (hp1 : p % 2 = 1) (ha0 : (a : zmodp p hp) ≠ 0) :
id                                                      └───┘  └┘  
src                                                       └───┘       
typ                                                     └───┘  └┘  
352    legendre_sym a p hp = (-1) ^ ((Ico 1 (p / 2).succ).filter
id     └──────────┘   └┘         └─┘        └──┘  └────┘
src    └──────────┘                └─┘         └──┘  └────┘
typ    └──────────┘   └┘         └─┘        └──┘  └────┘
doc                                   └─┘                └────┘
353      (λ x : ℕ, p / 2 < (a * x : zmodp p hp).val)).card :=
id                           └───┘  └┘ └─┘   └──┘
src                             └───┘      └─┘   └──┘
typ                          └───┘  └┘ └─┘   └──┘
doc                                                  └──┘
354  have (legendre_sym a p hp : zmodp p hp) = (((-1)^((Ico 1 (p / 2).succ).filter
id         └──────────┘   └┘   └───┘  └┘          └─┘        └──┘  └────┘
src        └──────────┘          └───┘               └─┘         └──┘  └────┘
typ        └──────────┘   └┘   └───┘  └┘          └─┘        └──┘  └────┘
doc                                                     └─┘                └────┘
355      (λ x : ℕ, p / 2 < (a * x : zmodp p hp).val)).card : ℤ) : zmodp p hp),
id                           └───┘  └┘ └─┘   └──┘        └───┘  └┘
src                             └───┘      └─┘   └──┘        └───┘
typ                          └───┘  └┘ └─┘   └──┘        └───┘  └┘
doc                                                  └──┘
356    by rw [legendre_sym_eq_pow, gauss_lemma_aux₂ hp hp1 ha0]; simp,
id            └─────────────────┘  └──────────────┘ └┘ └─┘ └─┘
src       └──┘└─────────────────┘└┘└──────────────┘          └──┘
typ       └──┘└─────────────────┘└┘└──────────────┘└┘└─┘└─┘  └──┘
doc       └──┘                   └┘                          └──┘
txt       └──┘                   └┘                          └──┘
par       └──┘                   └┘                          └──┘
pid         └┘                   └┘                        
st       └──────────────────────┘└───────────────────────────┘└────┘
357  begin
st   └─────
358    cases legendre_sym_eq_one_or_neg_one a hp ha0;
id           └────────────────────────────┘  └┘ └─┘
src    └────┘└────────────────────────────┘   
typ    └────┘└────────────────────────────┘└┘└─┘
doc    └────┘                                 
txt    └────┘                                 
par    └────┘                                 
pid                                          
st   ─────────────────────────────────────────────────
359    cases @neg_one_pow_eq_or ℤ _  ((Ico 1 (p / 2).succ).filter
id            └───────────────┘        └─┘      
src    └────┘ └───────────────┘ └──┘  └─┘└─┘  └────────────────
typ    └────┘ └───────────────┘ └──┘  └─┘└─┘  └────────────────
doc    └────┘                   └──┘  └─┘└─┘   └────────────────
txt    └────┘                   └──┘     └─┘   └────────────────
par    └────┘                   └──┘     └─┘   └────────────────
pid                            └──┘     └─┘   └────────────────
st   ─────────────────────────────────────────────────────────────
360      (λ x : ℕ, p / 2 < (a * x : zmodp p hp).val)).card;
id                               └───┘  └┘
src  ───┘  └───┘ └┘  └─┘   └─┘└───┘   └──────────┘
typ  ───┘  └───┘ └┘  └─┘  └─┘└───┘└┘└──────────┘
doc  ───┘  └───┘ └┘  └─┘     └─┘        └──────────┘
txt  ───┘  └───┘ └┘  └─┘     └─┘        └──────────┘
par  ───┘  └───┘ └┘  └─┘     └─┘        └──────────┘
pid  ───┘  └───┘ └┘  └─┘     └─┘        └─────────┘
st   ───────────────────────────────────────────────────────
361    simp [*, zmodp.ne_neg_self hp hp1 one_ne_zero,
id              └───────────────┘ └┘ └─┘ └─────────┘
src    └───────┘└───────────────┘     └─────────┘└─
typ    └───────┘└───────────────┘└┘└─┘└─────────┘└─
doc    └───────┘                                 └─
txt    └───────┘                                 └─
par    └───────┘                                 └─
pid        └──┘                                 └─
st   ─────────────────────────────────────────────────
362      (zmodp.ne_neg_self hp hp1 one_ne_zero).symm] at *
id        └───────────────┘ └┘ └─┘ └─────────┘
src  ───┘ └───────────────┘     └─────────┘└───────────┘
typ  ───┘ └───────────────┘└┘└─┘└─────────┘└───────────┘
doc  ───┘                                  └───────────┘
txt  ───┘                                  └───────────┘
par  ───┘                                  └───────────┘
pid  ───┘                                  └─────┘└──┘
st   ─────────────────────────────────────────────────────┘
363  end
st   └─┘
364  
365  lemma legendre_sym_eq_one_iff {a : ℕ} (ha0 : (a : zmodp p hp) ≠ 0) :
id                                                   └───┘  └┘  
src                                                   └───┘       
typ                                                  └───┘  └┘  
366    legendre_sym a p hp = 1 ↔ (∃ b : zmodp p hp, b ^ 2 = a) :=
id     └──────────┘   └┘           └───┘  └┘      
src    └──────────┘                  └───┘           
typ    └──────────┘   └┘           └───┘  └┘      
367  by rw [legendre_sym]; split_ifs; finish
id          └──────────┘
src     └──┘└──────────┘  └───────┘  └──────
typ     └──┘└──────────┘  └───────┘  └──────
doc     └──┘              └───────┘  └──────
txt     └──┘              └───────┘  └──────
par     └──┘              └───────┘  └──────
pid       └┘                               
st     └───────────────┘└───────────────────
368  
src  
typ  
doc  
txt  
par  
pid  
st   
369  lemma eisenstein_lemma (hp1 : p % 2 = 1) {a : ℕ} (ha1 : a % 2 = 1) (ha0 : (a : zmodp p hp) ≠ 0) :
id                                                                          └───┘  └┘  
src                                                                            └───┘       
typ                                                                         └───┘  └┘  
370    legendre_sym a p hp = (-1)^(Ico 1 (p / 2).succ).sum (λ x, (x * a) / p) :=
id     └──────────┘   └┘      └─┘        └──┘  └─┘             
src    └──────────┘             └─┘         └──┘  └─┘               
typ    └──────────┘   └┘      └─┘        └──┘  └─┘             
doc                                └─┘
371  by rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp hp1 ha0, neg_one_pow_eq_pow_mod_two,
id          └────────────────────────┘  └─────────┘ └┘ └─┘ └─┘  └────────────────────────┘
src     └──┘└────────────────────────┘└┘└─────────┘        └┘└────────────────────────┘└─
typ     └──┘└────────────────────────┘└┘└─────────┘└┘└─┘└─┘└┘└────────────────────────┘└─
doc     └──┘                          └┘└─────────┘        └┘                          └─
txt     └──┘                          └┘                   └┘                          └─
par     └──┘                          └┘                   └┘                          └─
pid       └┘                          └┘                   └┘                          └─
st     └─────────────────────────────┘└──────────────────────┘└──────────────────────────┘└─
372      show _ = _, from eisenstein_lemma_aux₂ hp hp1 ha1 ha0]
id                       └───────────────────┘ └┘ └─┘ └─┘ └─┘
src  ───┘    └─┘└───────┘└───────────────────┘           └─
typ  ───┘    └─┘└───────┘└───────────────────┘└┘└─┘└─┘└─┘└─
doc  ───┘    └─┘ └───────┘                                └─
txt  ───┘    └─┘ └───────┘                                └─
par  ───┘    └─┘ └───────┘                                └─
pid  ───┘    └─┘ └───────┘                                
st   ────────────────────────────────────────────────────────┘
373  
src  
typ  
doc  
txt  
par  
pid  
st   
374  theorem quadratic_reciprocity (hp1 : p % 2 = 1) (hq1 : q % 2 = 1) (hpq : p ≠ q) :
id                                                                        
src                                                                         
typ                                                                       
375    legendre_sym p q hq * legendre_sym q p hp = (-1) ^ ((p / 2) * (q / 2)) :=
id     └──────────┘   └┘  └──────────┘   └┘                 
src    └──────────┘         └──────────┘                          
typ    └──────────┘   └┘  └──────────┘   └┘                 
376  have hpq0 : (p : zmodp q hq) ≠ 0, from zmodp.prime_ne_zero _ hp hpq.symm,
id                   └───┘  └┘           └─────────────────┘   └┘ └─┘└───┘
src                   └───┘                └─────────────────┘         └───┘
typ                  └───┘  └┘           └─────────────────┘   └┘ └─┘└───┘
377  have hqp0 : (q : zmodp p hp) ≠ 0, from zmodp.prime_ne_zero _ hq hpq,
id                   └───┘  └┘           └─────────────────┘   └┘ └─┘
src                   └───┘                └─────────────────┘
typ                  └───┘  └┘           └─────────────────┘   └┘ └─┘
378  by rw [eisenstein_lemma _ hq1 hp1 hpq0, eisenstein_lemma _ hp1 hq1 hqp0,
id          └──────────────┘   └─┘ └─┘ └──┘  └──────────────┘   └─┘ └─┘ └──┘
src     └──┘└──────────────┘└─┘          └┘└──────────────┘└─┘          └─
typ     └──┘└──────────────┘└─┘└─┘└─┘└──┘└┘└──────────────┘└─┘└─┘└─┘└──┘└─
doc     └──┘                └─┘          └┘                └─┘          └─
txt     └──┘                └─┘          └┘                └─┘          └─
par     └──┘                └─┘          └┘                └─┘          └─
pid       └┘                └─┘          └┘                └─┘          └─
st     └──────────────────────────────────┘└───────────────────────────────┘└─
379    ← _root_.pow_add, sum_mul_div_add_sum_mul_div_eq_mul _ hpq0, mul_comm]
id       └────────────┘  └────────────────────────────────┘   └──┘  └──────┘
src  ───┘└────────────┘└┘└────────────────────────────────┘└─┘    └┘└──────┘└─
typ  ───┘└────────────┘└┘└────────────────────────────────┘└─┘└──┘└┘└──────┘└─
doc  ───┘              └┘└────────────────────────────────┘└─┘    └┘        └─
txt  ───┘              └┘                                  └─┘    └┘        └─
par  ───┘              └┘                                  └─┘    └┘        └─
pid  ───┘              └┘                                  └─┘    └┘        
st   ─────────────────┘└─────────────────────────────────────────┘└────────┘
380  
src  
typ  
doc  
txt  
par  
pid  
st   
381  lemma legendre_sym_two (hp1 : p % 2 = 1) : legendre_sym 2 p hp = (-1) ^ (p / 4 + p / 2) :=
id                                           └──────────┘    └┘              
src                                           └──────────┘                       
typ                                          └──────────┘    └┘              
382  have hp2 : p ≠ 2, from mt (congr_arg (% 2)) (by simp [hp1]),
id                        └┘  └───────┘                 └─┘
src                        └┘  └───────┘           └────┘   
typ                       └┘  └───────┘           └────┘└─┘
doc                                                  └────┘   
txt                                                  └────┘   
par                                                  └────┘   
pid                                                         
st                                                  └─────────┘
383  have hp22 : p / 2 / 2 = _ := div_eq_filter_card (show 0 < 2, from dec_trivial)
id                            └────────────────┘                  └─────────┘
src                            └────────────────┘                  └─────────┘
typ                           └────────────────┘                  └─────────┘
doc                                                                    └─────────┘
384    (nat.div_le_self (p / 2) 2),
id      └─────────────┘   
src     └─────────────┘    
typ     └─────────────┘   
385  have hcard : (Ico 1 (p / 2).succ).card = p / 2, by simp,
id                 └─┘        └──┘  └──┘    
src                └─┘         └──┘  └──┘            └──┘
typ                └─┘        └──┘  └──┘           └──┘
doc                └─┘                └──┘              └──┘
txt                                                     └──┘
par                                                     └──┘
st                                                     └───┘
386  have hx2 : ∀ x ∈ Ico 1 (p / 2).succ, (2 * x : zmodp p hp).val = 2 * x,
id                   └─┘        └──┘          └───┘  └┘ └─┘      
src                  └─┘         └──┘           └───┘      └─┘     
typ                  └─┘        └──┘          └───┘  └┘ └─┘      
doc                   └─┘
387    from λ x hx, have h2xp : 2 * x < p,
id             └┘                   
src                                  
typ            └┘                   
388        from calc 2 * x ≤ 2 * (p / 2) : mul_le_mul_of_nonneg_left
id                                    └───────────────────────┘
src                                     └───────────────────────┘
typ                                   └───────────────────────┘
389          (le_of_lt_succ $ by finish) dec_trivial
id            └───────────┘              └─────────┘
src           └───────────┘      └────┘  └─────────┘
typ           └───────────┘      └────┘  └─────────┘
doc                              └────┘  └─────────┘
txt                              └────┘
par                              └────┘
st                              └─────┘
390        ... < _ : by conv_rhs {rw [← mod_add_div p 2, add_comm, hp1]}; exact lt_succ_self _,
id                                      └─────────┘     └──────┘  └─┘          └──────────┘
src                     └────────┘└────┘└─────────┘ └──┘└──────┘└┘     └────┘└──────────┘└┘
typ                     └────────┘└────┘└─────────┘└──┘└──────┘└┘└─┘  └────┘└──────────┘└┘
doc                                                                       └────┘            └┘
txt                     └────────┘└────┘            └──┘        └┘     └────┘            └┘
par                     └────────┘└────┘            └──┘        └┘     └────┘            └┘
pid                             └─────┘            └──┘        └┘   └┘                   └┘
st                     └─────────┘└──────────────────┘└─────────┘└───┘ └┘└───────────────────┘
391      by rw [← nat.cast_two, ← nat.cast_mul, zmodp.val_cast_of_lt _ h2xp],
id                └──────────┘    └──────────┘  └──────────────────┘   └──┘
src         └────┘└──────────┘└──┘└──────────┘└┘└──────────────────┘└─┘    
typ         └────┘└──────────┘└──┘└──────────┘└┘└──────────────────┘└─┘└──┘
doc         └────┘            └──┘            └┘                    └─┘    
txt         └────┘            └──┘            └┘                    └─┘    
par         └────┘            └──┘            └┘                    └─┘    
pid           └──┘            └──┘            └┘                    └─┘    
st         └─────────────────┘└──────────────┘└───────────────────────────┘
392  have hdisj : disjoint
id                └──────┘
src               └──────┘
typ               └──────┘
doc               └──────┘
393      ((Ico 1 (p / 2).succ).filter (λ x, p / 2 < ((2 : ℕ) * x : zmodp p hp).val))
id         └─┘        └──┘  └────┘                        └───┘  └┘ └─┘
src        └─┘         └──┘  └────┘                           └───┘      └─┘
typ        └─┘        └──┘  └────┘                        └───┘  └┘ └─┘
doc        └─┘                └────┘
394      ((Ico 1 (p / 2).succ).filter (λ x, x * 2 ≤ p / 2)),
id         └─┘        └──┘  └────┘             
src        └─┘         └──┘  └────┘                
typ        └─┘        └──┘  └────┘             
doc        └─┘                └────┘
395    from disjoint_filter.2 (λ x hx, by simp [hx2 _ hx, mul_comm]),
id          └─────────────┘      └┘           └─┘   └┘  └──────┘
src         └─────────────┘              └────┘   └─┘  └┘└──────┘
typ         └─────────────┘      └┘     └────┘└─┘└─┘└┘└┘└──────┘
doc                                       └────┘   └─┘  └┘        
txt                                       └────┘   └─┘  └┘        
par                                       └────┘   └─┘  └┘        
pid                                              └─┘  └┘        
st                                       └────────────────────────┘
396  have hunion :
397      ((Ico 1 (p / 2).succ).filter (λ x, p / 2 < ((2 : ℕ) * x : zmodp p hp).val)) ∪
id         └─┘        └──┘  └────┘                        └───┘  └┘ └─┘    
src        └─┘         └──┘  └────┘                           └───┘      └─┘    
typ        └─┘        └──┘  └────┘                        └───┘  └┘ └─┘    
doc        └─┘                └────┘
398      ((Ico 1 (p / 2).succ).filter (λ x, x * 2 ≤ p / 2)) =
id         └─┘        └──┘  └────┘                  
src        └─┘         └──┘  └────┘                     
typ        └─┘        └──┘  └────┘                  
doc        └─┘                └────┘
399      Ico 1 (p / 2).succ,
id       └─┘        └──┘
src      └─┘         └──┘
typ      └─┘        └──┘
doc      └─┘
400    begin
st     └─────
401      rw [filter_union_right],
id           └────────────────┘
src      └──┘└────────────────┘
typ      └──┘└────────────────┘
doc      └──┘                  
txt      └──┘                  
par      └──┘                  
pid        └┘                  
st   ─────────────────────────┘└──
402      conv_rhs {rw [← @filter_true _ (Ico 1 (p / 2).succ)]},
id                        └─────────┘    └─┘     
src      └────────┘└────┘ └─────────┘└─┘ └─┘└─┘  └────────┘
typ      └────────┘└────┘ └─────────┘└─┘ └─┘└─┘ └────────┘
doc                                      └─┘
txt      └────────┘└────┘            └─┘    └─┘   └────────┘
par      └────────┘└────┘            └─┘    └─┘   └────────┘
pid              └─────┘            └─┘    └─┘   └─────────┘
st   ─────────────┘└───────────────────────────────────────┘ └┘
403      exact filter_congr (λ x hx, by simp [hx2 _ hx, lt_or_le, mul_comm])
id             └──────────┘                   └─┘   └┘  └──────┘  └──────┘
src      └────┘└──────────┘  └─────┘  └────┘   └─┘  └┘└──────┘└┘└──────┘└─
typ      └────┘└──────────┘  └─────┘  └────┘└─┘└─┘└┘└┘└──────┘└┘└──────┘└─
doc      └────┘              └─────┘  └────┘   └─┘  └┘        └┘        └─
txt      └────┘              └─────┘  └────┘   └─┘  └┘        └┘        └─
par      └────┘              └─────┘  └────┘   └─┘  └┘        └┘        └─
pid                         └─────┘  └─────┘   └─┘  └┘        └┘        └┘
st   ─────────────────────────────────┘└──────────────────────────────────┘└─
404    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
405  begin
st   └─────
406    rw [gauss_lemma _ hp1 (prime_ne_zero hp prime_two hp2),
id         └─────────┘   └─┘  └───────────┘ └┘ └───────┘ └─┘
src    └──┘└─────────┘└─┘    └───────────┘  └───────┘   └──
typ    └──┘└─────────┘└─┘└─┘ └───────────┘└┘└───────┘└─┘└──
doc    └──┘└─────────┘└─┘                               └──
txt    └──┘           └─┘                               └──
par    └──┘           └─┘                               └──
pid      └┘           └─┘                               └──
st   ───────────────────────────────────────────────────────┘└─
407      neg_one_pow_eq_pow_mod_two, @neg_one_pow_eq_pow_mod_two _ _ (p / 4 + p / 2)],
id       └────────────────────────┘   └────────────────────────┘             
src  ───┘└────────────────────────┘└┘ └────────────────────────┘└───┘   └─┘  └──┘
typ  ───┘└────────────────────────┘└┘ └────────────────────────┘└───┘   └─┘ └──┘
doc  ───┘                          └┘                           └───┘   └─┘   └──┘
txt  ───┘                          └┘                           └───┘   └─┘   └──┘
par  ───┘                          └┘                           └───┘   └─┘   └──┘
pid  ───┘                          └┘                           └───┘   └─┘   └──┘
st   ─────────────────────────────┘└───────────────────────────────────────────────┘└──
408    refine congr_arg2 _ rfl ((@zmod.eq_iff_modeq_nat 2 _ _).1 _),
id            └────────┘   └─┘    └───────────────────┘
src    └─────┘└────────┘└─┘└─┘   └───────────────────┘└──────────┘
typ    └─────┘└────────┘└─┘└─┘   └───────────────────┘└──────────┘
doc    └─────┘          └─┘                           └──────────┘
txt    └─────┘          └─┘                           └──────────┘
par    └─────┘          └─┘                           └──────────┘
pid                    └─┘                           └──────────┘
st   ─────────────────────────────────────────────────────────────┘└─
409    rw [show 4 = 2 * 2, from rfl, ← nat.div_div_eq_div_mul, hp22, nat.cast_add,
id                            └─┘    └────────────────────┘  └──┘  └──────────┘
src    └──┘    └─┘└─┘└───────┘└─┘└──┘└────────────────────┘└┘    └┘└──────────┘└─
typ    └──┘    └─┘└─┘└───────┘└─┘└──┘└────────────────────┘└┘└──┘└┘└──────────┘└─
doc    └──┘    └─┘ └─┘ └───────┘   └──┘                      └┘    └┘            └─
txt    └──┘    └─┘ └─┘ └───────┘   └──┘                      └┘    └┘            └─
par    └──┘    └─┘ └─┘ └───────┘   └──┘                      └┘    └┘            └─
pid      └┘    └─┘ └─┘ └───────┘   └──┘                      └┘    └┘            └─
st   ─────────────────────────────┘└────────────────────────┘└────┘└────────────┘└─
410      ← sub_eq_iff_eq_add', sub_eq_add_neg, zmod.neg_eq_self_mod_two,
id         └────────────────┘  └────────────┘  └──────────────────────┘
src  ─────┘└────────────────┘└┘└────────────┘└┘└──────────────────────┘└─
typ  ─────┘└────────────────┘└┘└────────────┘└┘└──────────────────────┘└─
doc  ─────┘                  └┘              └┘                        └─
txt  ─────┘                  └┘              └┘                        └─
par  ─────┘                  └┘              └┘                        └─
pid  ─────┘                  └┘              └┘                        └─
st   ───────────────────────┘└──────────────┘└────────────────────────┘└─
411      ← nat.cast_add, ← card_disjoint_union hdisj, hunion, hcard]
id         └──────────┘    └─────────────────┘ └───┘  └────┘  └───┘
src  ─────┘└──────────┘└──┘└─────────────────┘     └┘      └┘     └┘
typ  ─────┘└──────────┘└──┘└─────────────────┘└───┘└┘└────┘└┘└───┘└┘
doc  ─────┘            └──┘                        └┘      └┘     └┘
txt  ─────┘            └──┘                        └┘      └┘     └┘
par  ─────┘            └──┘                        └┘      └┘     └┘
pid  ─────┘            └──┘                        └┘      └┘     
st   ─────────────────┘└───────────────────────────┘└──────┘└─────┘
412  end
st   └─┘
413  
414  lemma exists_pow_two_eq_two_iff (hp1 : p % 2 = 1) :
id                                              
src                                              
typ                                             
415    (∃ a : zmodp p hp, a ^ 2 = 2) ↔ p % 8 = 1 ∨ p % 8 = 7 :=
id           └───┘  └┘                      
src          └───┘                              
typ          └───┘  └┘                      
416  have hp2 : ((2 : ℕ) : zmodp p hp) ≠ 0,
id                        └───┘  └┘  
src                       └───┘       
typ                       └───┘  └┘  
417    from zmodp.prime_ne_zero hp prime_two (λ h, by simp * at *),
id          └─────────────────┘ └┘ └───────┘    
src         └─────────────────┘    └───────┘          └─────────┘
typ         └─────────────────┘ └┘ └───────┘         └─────────┘
doc                                                   └─────────┘
txt                                                   └─────────┘
par                                                   └─────────┘
pid                                                       └──┘
st                                                   └──────────┘
418  have hpm4 : p % 4 = p % 8 % 4, from (nat.mod_mul_left_mod p 2 4).symm,
id                                  └──────────────────┘      └──┘
src                                   └──────────────────┘       └──┘
typ                                 └──────────────────┘      └──┘
419  have hpm2 : p % 2 = p % 8 % 2, from (nat.mod_mul_left_mod p 4 2).symm,
id                                  └──────────────────┘      └──┘
src                                   └──────────────────┘       └──┘
typ                                 └──────────────────┘      └──┘
420  begin
st   └─────
421    rw [show (2 : zmodp p hp) = (2 : ℕ), by simp, ← legendre_sym_eq_one_iff hp hp2,
id                   └───┘  └┘                       └─────────────────────┘ └┘ └─┘
src    └──┘     └──┘└───┘   └┘ └──┘ └────┘└──┘└──┘└─────────────────────┘     └─
typ    └──┘     └──┘└───┘└┘└┘ └──┘ └────┘└──┘└──┘└─────────────────────┘└┘└─┘└─
doc    └──┘     └──┘        └┘  └──┘ └────┘└──┘└──┘                            └─
txt    └──┘     └──┘        └┘  └──┘ └────┘└──┘└──┘                            └─
par    └──┘     └──┘        └┘  └──┘ └────┘└──┘└──┘                            └─
pid      └┘     └──┘        └┘  └──┘ └────────────┘                            └─
st   ────────────────────────────────────────┘└───┘└────────────────────────────────┘└─
422      legendre_sym_two hp hp1, neg_one_pow_eq_one_iff_even (show (-1 : ℤ) ≠ 1, from dec_trivial),
id       └──────────────┘ └┘ └─┘  └─────────────────────────┘                        └─────────┘
src  ───┘└──────────────┘     └┘└─────────────────────────┘      └──┘ └┘└───────┘└─────────┘└──
typ  ───┘└──────────────┘└┘└─┘└┘└─────────────────────────┘      └──┘ └┘└───────┘└─────────┘└──
doc  ───┘                     └┘                                  └──┘ └┘ └───────┘└─────────┘└──
txt  ───┘                     └┘                                  └──┘ └┘ └───────┘           └──
par  ───┘                     └┘                                  └──┘ └┘ └───────┘           └──
pid  ───┘                     └┘                                  └──┘ └┘ └───────┘           └──
st   ──────────────────────────┘└─────────────────────────────────────────────────────────────────┘└─
423      even_add, even_div, even_div],
id       └──────┘  └──────┘  └──────┘
src  ───┘└──────┘└┘└──────┘└┘└──────┘
typ  ───┘└──────┘└┘└──────┘└┘└──────┘
doc  ───┘        └┘        └┘        
txt  ───┘        └┘        └┘        
par  ───┘        └┘        └┘        
pid  ───┘        └┘        └┘        
st   ───────────┘└────────┘└────────┘└──
424    have := nat.mod_lt p (show 0 < 8, from dec_trivial),
id             └────────┘          
src    └──────┘└────────┘      └─┘└───────┘           
typ    └──────┘└────────┘     └─┘└───────┘           
doc    └──────┘                └─┘ └───────┘           
txt    └──────┘                └─┘ └───────┘           
par    └──────┘                └─┘ └───────┘           
pid    └───┘└─┘                └─┘ └───────┘           
st   ────────────────────────────────────────────────────┘└─
425    revert this hp1,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid          └───────┘
st   ────────────────┘└─
426    erw [hpm4, hpm2],
id          └──┘  └──┘
src    └───┘    └┘    
typ    └───┘└──┘└┘└──┘
doc    └───┘    └┘    
txt    └───┘    └┘    
par    └───┘    └┘    
pid       └┘    └┘    
st   ──────────┘└────┘└──
427    generalize hm : p % 8 = m,
id                      
src    └──────────────┘ └─┘ 
typ    └──────────────┘└─┘ 
doc    └──────────────┘  └─┘ 
txt    └──────────────┘  └─┘ 
par    └──────────────┘  └─┘ 
pid              └─┘└┘  └─┘ 
st   ──────────────────────────┘└─
428    clear hm,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid         └─┘
st   ─────────┘└─
429    revert m,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          └┘
st   ─────────┘└─
430    exact dec_trivial
src    └────┘           
typ    └────┘           
doc    └────┘           
txt    └────┘           
par    └────┘           
pid                    
st   ───────────────────┘
431  end
st   └─┘
432  
433  lemma exists_pow_two_eq_prime_iff_of_mod_four_eq_one (hp1 : p % 4 = 1) (hq1 : q % 2 = 1) :
id                                                                                  
src                                                                                   
typ                                                                                 
434    (∃ a : zmodp p hp, a ^ 2 = q) ↔ ∃ b : zmodp q hq, b ^ 2 = p :=
id           └───┘  └┘              └───┘  └┘      
src          └───┘                     └───┘           
typ          └───┘  └┘              └───┘  └┘      
435  if hpq : p = q then by resetI; subst hpq else
id   └┘                                └─┘
src  └┘                    └────┘  └────┘   
typ  └┘                  └────┘  └────┘└─┘
doc                         └────┘  └────┘   
txt                         └────┘  └────┘   
par                         └────┘  └────┘   
pid                                         
st                         └─────────────────┘
436  have h1 : ((p / 2) * (q / 2)) % 2 = 0,
id   └──┘                        
src                                
typ  └──┘                        
437    from (dvd_iff_mod_eq_zero _ _).1
id           └─────────────────┘     
src          └─────────────────┘     
typ          └─────────────────┘     
438      (dvd_mul_of_dvd_left ((dvd_iff_mod_eq_zero _ _).2 $
id        └─────────────────┘   └─────────────────┘     
src       └─────────────────┘   └─────────────────┘     
typ       └─────────────────┘   └─────────────────┘     
439      by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hp1]; refl) _),
id                └────────────────────┘                     └─┘  └─┘
src         └────┘└────────────────────┘└┘    └─┘└─┘└───────┘└─┘└┘     └──┘
typ         └────┘└────────────────────┘└┘    └─┘└─┘└───────┘└─┘└┘└─┘  └──┘
doc         └────┘                      └┘    └─┘ └─┘ └───────┘   └┘     └──┘
txt         └────┘                      └┘    └─┘ └─┘ └───────┘   └┘     └──┘
par         └────┘                      └┘    └─┘ └─┘ └───────┘   └┘     └──┘
pid           └──┘                      └┘    └─┘ └─┘ └───────┘   └┘   
st         └───────────────────────────┘└────────────────────────┘└───┘└────┘
440  begin
st   └─────
441    have := quadratic_reciprocity hp hq (odd_of_mod_four_eq_one hp1) hq1 hpq,
id             └───────────────────┘ └┘ └┘  └────────────────────┘ └─┘  └─┘ └─┘
src    └──────┘└───────────────────┘     └────────────────────┘   └┘   
typ    └──────┘└───────────────────┘└┘└┘ └────────────────────┘└─┘└┘└─┘└─┘
doc    └──────┘                                                   └┘   
txt    └──────┘                                                   └┘   
par    └──────┘                                                   └┘   
pid    └───┘└─┘                                                   └┘   
st   ─────────────────────────────────────────────────────────────────────────┘└─
442    rw [neg_one_pow_eq_pow_mod_two, h1, legendre_sym, legendre_sym,
id         └────────────────────────┘  └┘  └──────────┘  └──────────┘
src    └──┘└────────────────────────┘└┘  └┘└──────────┘└┘└──────────┘└─
typ    └──┘└────────────────────────┘└┘└┘└┘└──────────┘└┘└──────────┘└─
doc    └──┘                          └┘  └┘            └┘            └─
txt    └──┘                          └┘  └┘            └┘            └─
par    └──┘                          └┘  └┘            └┘            └─
pid      └┘                          └┘  └┘            └┘            └─
st   ───────────────────────────────┘└──┘└────────────┘└────────────┘└─
443      if_neg (zmodp.prime_ne_zero hp hq hpq),
id       └────┘  └─────────────────┘ └┘ └┘ └─┘
src  ───┘└────┘ └─────────────────┘       └──
typ  ───┘└────┘ └─────────────────┘└┘└┘└─┘└──
doc  ───┘                                 └──
txt  ───┘                                 └──
par  ───┘                                 └──
pid  ───┘                                 └──
st   ─────────────────────────────────────────┘└─
444      if_neg (zmodp.prime_ne_zero hq hp (ne.symm hpq))] at this,
id       └────┘  └─────────────────┘ └┘ └┘  └─────┘ └─┘
src  ───┘└────┘ └─────────────────┘     └─────┘   └─────────┘
typ  ───┘└────┘ └─────────────────┘└┘└┘ └─────┘└─┘└─────────┘
doc  ───┘                                         └─────────┘
txt  ───┘                                         └─────────┘
par  ───┘                                         └─────────┘
pid  ───┘                                         └─┘└──────┘
st   ───────────────────────────────────────────────────┘└──────┘└─
445    split_ifs at this; simp *; contradiction
src    └───────────────┘  └────┘  └────────────┘
typ    └───────────────┘  └────┘  └────────────┘
doc    └───────────────┘  └────┘  └────────────┘
txt    └───────────────┘  └────┘  └────────────┘
par    └───────────────┘  └────┘  └────────────┘
pid             └──────┘                     
st   ──────────────────────────────────────────┘
446  end
st   └─┘
447  
448  lemma exists_pow_two_eq_prime_iff_of_mod_four_eq_three (hp3 : p % 4 = 3)
id                                                                     
src                                                                     
typ                                                                    
449    (hq3 : q % 4 = 3) (hpq : p ≠ q) : (∃ a : zmodp p hp, a ^ 2 = q) ↔ ¬∃ b : zmodp q hq, b ^ 2 = p :=
id                                       └───┘  └┘              └───┘  └┘      
src                                         └───┘                     └───┘           
typ                                      └───┘  └┘              └───┘  └┘      
450  have h1 : ((p / 2) * (q / 2)) % 2 = 1,
id                               
src                                
typ                              
451    from nat.odd_mul_odd
id          └─────────────┘
src         └─────────────┘
typ         └─────────────┘
452      (by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hp3]; refl)
id                 └────────────────────┘                     └─┘  └─┘
src          └────┘└────────────────────┘└┘    └─┘└─┘└───────┘└─┘└┘     └──┘
typ          └────┘└────────────────────┘└┘    └─┘└─┘└───────┘└─┘└┘└─┘  └──┘
doc          └────┘                      └┘    └─┘ └─┘ └───────┘   └┘     └──┘
txt          └────┘                      └┘    └─┘ └─┘ └───────┘   └┘     └──┘
par          └────┘                      └┘    └─┘ └─┘ └───────┘   └┘     └──┘
pid            └──┘                      └┘    └─┘ └─┘ └───────┘   └┘   
st          └───────────────────────────┘└────────────────────────┘└───┘└────┘
453      (by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hq3]; refl),
id                 └────────────────────┘                       └─┘  └─┘
src          └────┘└────────────────────┘└┘    └─┘ └─┘ └───────┘└─┘└┘     └──┘
typ          └────┘└────────────────────┘└┘    └─┘ └─┘ └───────┘└─┘└┘└─┘  └──┘
doc          └────┘                      └┘    └─┘ └─┘ └───────┘   └┘     └──┘
txt          └────┘                      └┘    └─┘ └─┘ └───────┘   └┘     └──┘
par          └────┘                      └┘    └─┘ └─┘ └───────┘   └┘     └──┘
pid            └──┘                      └┘    └─┘ └─┘ └───────┘   └┘   
st          └───────────────────────────┘└────────────────────────┘└───┘└────┘
454  begin
st   └─────
455    have := quadratic_reciprocity hp hq (odd_of_mod_four_eq_three hp3)
id             └───────────────────┘ └┘ └┘                           └─┘
src    └──────┘└───────────────────┘                                └─
typ    └──────┘└───────────────────┘└┘└┘                         └─┘└─
doc    └──────┘                                                     └─
txt    └──────┘                                                     └─
par    └──────┘                                                     └─
pid    └───┘└─┘                                                     └─
st   ─────────────────────────────────────────────────────────────────────
456      (odd_of_mod_four_eq_three hq3) hpq,
id        └──────────────────────┘ └─┘  └─┘
src  ───┘ └──────────────────────┘   └┘
typ  ───┘ └──────────────────────┘└─┘└┘└─┘
doc  ───┘                            └┘
txt  ───┘                            └┘
par  ───┘                            └┘
pid  ───┘                            └┘
st   ─────────────────────────────────────┘└─
457    rw [neg_one_pow_eq_pow_mod_two, h1, legendre_sym, legendre_sym,
id         └────────────────────────┘  └┘  └──────────┘  └──────────┘
src    └──┘└────────────────────────┘└┘  └┘└──────────┘└┘└──────────┘└─
typ    └──┘└────────────────────────┘└┘└┘└┘└──────────┘└┘└──────────┘└─
doc    └──┘                          └┘  └┘            └┘            └─
txt    └──┘                          └┘  └┘            └┘            └─
par    └──┘                          └┘  └┘            └┘            └─
pid      └┘                          └┘  └┘            └┘            └─
st   ───────────────────────────────┘└──┘└────────────┘└────────────┘└─
458      if_neg (zmodp.prime_ne_zero hp hq hpq),
id       └────┘  └─────────────────┘ └┘ └┘ └─┘
src  ───┘└────┘ └─────────────────┘       └──
typ  ───┘└────┘ └─────────────────┘└┘└┘└─┘└──
doc  ───┘                                 └──
txt  ───┘                                 └──
par  ───┘                                 └──
pid  ───┘                                 └──
st   ─────────────────────────────────────────┘└─
459      if_neg (zmodp.prime_ne_zero hq hp hpq.symm)] at this,
id       └────┘  └─────────────────┘ └┘ └┘ └──────┘
src  ───┘└────┘ └─────────────────┘    └──────┘└────────┘
typ  ───┘└────┘ └─────────────────┘└┘└┘└──────┘└────────┘
doc  ───┘                                      └────────┘
txt  ───┘                                      └────────┘
par  ───┘                                      └────────┘
pid  ───┘                                      └┘└──────┘
st   ──────────────────────────────────────────────┘└──────┘└─
460    split_ifs at this; simp *; contradiction
src    └───────────────┘  └────┘  └────────────┘
typ    └───────────────┘  └────┘  └────────────┘
doc    └───────────────┘  └────┘  └────────────┘
txt    └───────────────┘  └────┘  └────────────┘
par    └───────────────┘  └────┘  └────────────┘
pid             └──────┘                     
st   ──────────────────────────────────────────┘
461  end
st   └─┘
462  
463  end zmodp